-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmake.ml
35 lines (29 loc) · 2.26 KB
/
make.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
(* ========================================================================= *)
(* HOL-Light Library for Modal Systems *)
(* *)
(* (c) Copyright, Marco Maggesi, Cosimo Perini Brogi 2020-2022. *)
(* (c) Copyright, Antonella Bilotta, Marco Maggesi, *)
(* Cosimo Perini Brogi, Leonardo Quartini 2024. *)
(* ========================================================================= *)
(* ------------------------------------------------------------------------- *)
(* Libraries. *)
(* ------------------------------------------------------------------------- *)
needs "Library/card.ml";; (* Cardinality *)
needs "Library/rstc.ml";; (* Refl, sym, trans closure *)
(* ------------------------------------------------------------------------- *)
(* Syntax, semantics and calculus. *)
(* ------------------------------------------------------------------------- *)
loadt "HOLMS/misc.ml";; (* Miscellanea *)
loadt "HOLMS/modal.ml";; (* Syntax and semantics *)
loadt "HOLMS/calculus.ml";; (* Axiomatic calculus *)
(* ------------------------------------------------------------------------- *)
(* Meta-theory. *)
(* ------------------------------------------------------------------------- *)
loadt "HOLMS/conjlist.ml";; (* Iterated conjunctions *)
loadt "HOLMS/consistent.ml";; (* Consistent sets of formulae *)
loadt "HOLMS/gen_completness.ml";; (* Lemmata about completeness *)
loadt "HOLMS/k_completeness.ml";; (* Completeness of K *)
loadt "HOLMS/gl_completeness.ml";; (* Completeness of GL *)
loadt "HOLMS/gen_decid.ml";; (* Lemmata about decidability *)
loadt "HOLMS/gl_decid.ml";; (* Semidecision procedure for GL *)
loadt "HOLMS/k_decid.ml";; (* Semidecision procedure for K *)