changeset 9000 | c20d58286a51 |
parent 6349 | f7750d816c21 |
child 15531 | 08c8dad8e399 |
--- a/src/LCF/ex/ROOT.ML Tue May 30 16:03:09 2000 +0200 +++ b/src/LCF/ex/ROOT.ML Tue May 30 16:08:38 2000 +0200 @@ -6,10 +6,7 @@ Some examples from Lawrence Paulson's book Logic and Computation. *) -writeln"Root file for LCF examples"; - -set proof_timing; -use_thy "Ex1"; -use_thy "Ex2"; -use_thy "Ex3"; -use_thy "Ex4"; +time_use_thy "Ex1"; +time_use_thy "Ex2"; +time_use_thy "Ex3"; +time_use_thy "Ex4";