changeset 1465 | 5d7a7e439cec |
parent 1351 | 4a960c012383 |
child 4137 | 2ce2e659c2b1 |
--- a/src/HOL/Lex/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Lex/ROOT.ML Tue Jan 30 15:24:36 1996 +0100 @@ -1,9 +1,9 @@ -(* Title: HOL/Lex/ROOT.ML +(* Title: HOL/Lex/ROOT.ML ID: $Id$ - Author: Tobias Nipkow + Author: Tobias Nipkow Copyright 1995 TUM *) -HOL_build_completed; (*Make examples fail if HOL did*) +HOL_build_completed; (*Make examples fail if HOL did*) use_thy"AutoChopper";