--- a/src/ZF/ex/ROOT.ML Wed Mar 15 12:52:03 1995 +0100
+++ b/src/ZF/ex/ROOT.ML Thu Mar 16 00:00:30 1995 +0100
@@ -8,38 +8,37 @@
ZF_build_completed; (*Make examples fail if ZF did*)
-(writeln"Root file for ZF Set Theory examples";
- proof_timing := true;
+writeln"Root file for ZF Set Theory examples";
+proof_timing := true;
- loadpath := [".", "ex"];
+loadpath := [".", "ex"];
- time_use "ex/misc.ML";
- time_use_thy "ex/Ramsey";
+time_use "ex/misc.ML";
+time_use_thy "ex/Ramsey";
- (*Integers & Binary integer arithmetic*)
- time_use_thy "ex/Bin";
+(*Integers & Binary integer arithmetic*)
+time_use_thy "ex/Bin";
- (** Datatypes **)
- time_use_thy "ex/BT"; (*binary trees*)
- time_use_thy "ex/Data"; (*Sample datatype*)
- time_use_thy "ex/Term"; (*terms: recursion over the list functor*)
- time_use_thy "ex/TF"; (*trees/forests: mutual recursion*)
- time_use_thy "ex/Ntree"; (*variable-branching trees; function demo*)
- time_use_thy "ex/Brouwer"; (*Infinite-branching trees*)
- time_use_thy "ex/Enum"; (*Enormous enumeration type*)
+(** Datatypes **)
+time_use_thy "ex/BT"; (*binary trees*)
+time_use_thy "ex/Data"; (*Sample datatype*)
+time_use_thy "ex/Term"; (*terms: recursion over the list functor*)
+time_use_thy "ex/TF"; (*trees/forests: mutual recursion*)
+time_use_thy "ex/Ntree"; (*variable-branching trees; function demo*)
+time_use_thy "ex/Brouwer"; (*Infinite-branching trees*)
+time_use_thy "ex/Enum"; (*Enormous enumeration type*)
- (** Inductive definitions **)
- time_use_thy "ex/Rmap"; (*mapping a relation over a list*)
- time_use_thy "ex/PropLog"; (*completeness of propositional logic*)
- (*two Coq examples by Christine Paulin-Mohring*)
- time_use_thy "ex/ListN";
- time_use_thy "ex/Acc";
- time_use_thy "ex/Comb"; (*Combinatory Logic example*)
- time_use_thy "ex/Primrec"; (*Primitive recursive functions*)
+(** Inductive definitions **)
+time_use_thy "ex/Rmap"; (*mapping a relation over a list*)
+time_use_thy "ex/PropLog"; (*completeness of propositional logic*)
+(*two Coq examples by Christine Paulin-Mohring*)
+time_use_thy "ex/ListN";
+time_use_thy "ex/Acc";
+time_use_thy "ex/Comb"; (*Combinatory Logic example*)
+time_use_thy "ex/Primrec"; (*Primitive recursive functions*)
- (** CoDatatypes **)
- time_use_thy "ex/LList";
- time_use_thy "ex/CoUnit";
+(** CoDatatypes **)
+time_use_thy "ex/LList";
+time_use_thy "ex/CoUnit";
- writeln"END: Root file for ZF Set Theory examples"
-) handle _ => exit 1;
+writeln"END: Root file for ZF Set Theory examples";