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