changeset 1465 | 5d7a7e439cec |
parent 1447 | bc2c0acbbf29 |
child 1696 | e84bff5c519b |
--- a/src/HOL/IMP/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/IMP/ROOT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,10 +1,10 @@ -(* Title: HOL/IMP/ROOT.ML +(* Title: HOL/IMP/ROOT.ML ID: $Id$ - Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow + Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow Copyright 1995 TUM *) -HOL_build_completed; (*Make examples fail if HOL did*) +HOL_build_completed; (*Make examples fail if HOL did*) writeln"Root file for HOL/IMP"; proof_timing := true;