Update from HH

[Gödel's incompleteness theorem/.git] / make.ml

diff --git a/make.ml b/make.ml
new file mode 100644 (file)
index 0000000..acbacd1
--- /dev/null
+++ b/make.ml
@@ -0,0 +1,24 @@
+prioritize_num();;
+
+(* ------------------------------------------------------------------------- *)
+(* Some additional mathematical background.                                  *)
+(* ------------------------------------------------------------------------- *)
+
+loadt "Library/rstc.ml";;
+loadt "Library/prime.ml";;
+
+(* ------------------------------------------------------------------------- *)
+(* The basics of first order logic and our inference system.                 *)
+(* ------------------------------------------------------------------------- *)
+
+loadt "Arithmetic/fol.ml";;
+loadt "Arithmetic/derived.ml";;
+
+(* ------------------------------------------------------------------------- *)
+(* The incompleteness results.                                               *)
+(* ------------------------------------------------------------------------- *)
+
+loadt "Arithmetic/definability.ml";;
+loadt "Arithmetic/tarski.ml";;
+loadt "Arithmetic/arithprov.ml";;
+loadt "Arithmetic/godel.ml";;