1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(* ========================================================================= *)
(* Consistency proof of "pure HOL" (no axioms or definitions) in itself. *)
(* ========================================================================= *)
loadt "Library/card.ml";;
(* ------------------------------------------------------------------------- *)
(* Syntactic definitions (terms, types, theorems etc.) *)
(* ------------------------------------------------------------------------- *)
loadt "Model/syntax.ml";;
(* ------------------------------------------------------------------------- *)
(* Set-theoretic hierarchy to support semantics. *)
(* ------------------------------------------------------------------------- *)
loadt "Model/modelset.ml";;
(* ------------------------------------------------------------------------- *)
(* Semantics. *)
(* ------------------------------------------------------------------------- *)
loadt "Model/semantics.ml";;
|
