isabelle: src/HOL/IMP/ROOT.ML@b2463861c86a (annotated)

1465 5d7a7e439cec expanded tabs clasohm parents: 1447 diff changeset	1	(* Title: HOL/IMP/ROOT.ML
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	2	ID: $Id$
1465 5d7a7e439cec expanded tabs clasohm parents: 1447 diff changeset	3	Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow
936 a6d7b4084761 Hoare logic nipkow parents: 924 diff changeset	4	Copyright 1995 TUM
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	5	*)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	6
1465 5d7a7e439cec expanded tabs clasohm parents: 1447 diff changeset	7	HOL_build_completed; (Make examples fail if HOL did)
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	8
1165 97b2bb5d43c3 renamed CHOL to HOL clasohm parents: 1025 diff changeset	9	writeln"Root file for HOL/IMP";
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	10	proof_timing := true;
1696 e84bff5c519b A completely new version of IMP. nipkow parents: 1465 diff changeset	11	time_use_thy "Expr";
e84bff5c519b A completely new version of IMP. nipkow parents: 1465 diff changeset	12	time_use_thy "Transition";
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: 1351 diff changeset	13	time_use_thy "VC";