changeset 4446 | 097004a470fb |
parent 2601 | b301958c465d |
child 6349 | f7750d816c21 |
--- a/src/FOL/ex/ROOT.ML Fri Dec 19 10:17:04 1997 +0100 +++ b/src/FOL/ex/ROOT.ML Fri Dec 19 10:18:03 1997 +0100 @@ -10,7 +10,7 @@ FOL_build_completed; (*Cause examples to fail if FOL did*) -proof_timing := true; +set proof_timing; time_use "intro.ML"; time_use_thy "Nat"; @@ -39,7 +39,3 @@ writeln"\n** How to declare an oracle **\n"; time_use_thy "IffOracle"; - - -OS.FileSys.chDir ".."; -maketest"END: Root file for FOL examples";