colo12-c703.uibk.ac.at Git - Model of HOL/.git/blob - 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";;