changeset 1465 | 5d7a7e439cec |
parent 1363 | 7bdc4699ef4d |
child 5646 | 7c2ddbaf8b8c |
--- a/src/HOL/Hoare/ROOT.ML Tue Jan 30 15:19:20 1996 +0100 +++ b/src/HOL/Hoare/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: 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 "Examples"; use_thy "List_Examples";