isabelle: src/HOL/IMP/ROOT.ML@8b4acb408301 (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
6349 f7750d816c21 removed foo_build_completed -- now handled by session management (via usedir); wenzelm parents: 4449 diff changeset	7	writeln"Root file for HOL/IMP";
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	8
4449 df30e75f670f tuned; wenzelm parents: 1696 diff changeset	9	set proof_timing;
1696 e84bff5c519b A completely new version of IMP. nipkow parents: 1465 diff changeset	10	time_use_thy "Expr";
e84bff5c519b A completely new version of IMP. nipkow parents: 1465 diff changeset	11	time_use_thy "Transition";
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: 1351 diff changeset	12	time_use_thy "VC";