changeset 4449 | df30e75f670f |
parent 1696 | e84bff5c519b |
child 6349 | f7750d816c21 |
--- a/src/HOL/IMP/ROOT.ML Fri Dec 19 10:27:23 1997 +0100 +++ b/src/HOL/IMP/ROOT.ML Fri Dec 19 10:28:33 1997 +0100 @@ -7,7 +7,7 @@ HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/IMP"; -proof_timing := true; +set proof_timing; time_use_thy "Expr"; time_use_thy "Transition"; time_use_thy "VC";