# HG changeset patch
# User lcp
# Date 793965236 -3600
# Node ID 49271bd72c42b22bc0c8f118252997980cf3269f
# Parent  7ecdff86a5f069b226e3ae4c7c965a22c99f629a
No longer calls maketest; instead, the Makefile writes the file
test.

diff -r 7ecdff86a5f0 -r 49271bd72c42 src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Tue Feb 28 10:51:52 1995 +0100
+++ b/src/ZF/ex/ROOT.ML	Tue Feb 28 10:53:56 1995 +0100
@@ -3,42 +3,43 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Executes all examples for Zermelo-Fraenkel Set Theory
+Executes miscellaneous examples for Zermelo-Fraenkel Set Theory
 *)
 
 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";
 
-maketest"END: Root file for ZF Set Theory examples";
+ writeln"END: Root file for ZF Set Theory examples"
+)  handle _ => exit 1;