src/LCF/ex/ROOT.ML
changeset 2820 6303966dce96
child 4446 097004a470fb
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/LCF/ex/ROOT.ML	Thu Mar 20 11:09:01 1997 +0100
@@ -0,0 +1,10 @@
+
+writeln"Root file for LCF examples";
+LCF_build_completed;    (*Cause examples to fail if LCF did*)
+
+proof_timing := true;
+
+use"ex.ML";
+
+cd "..";
+maketest"END: file for LCF examples";