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

9277 a0a7c31cdc39 added dependency caveat oheimb parents: 9276 diff changeset	1	(* Title: HOL/IMP/ROOT.ML
a0a7c31cdc39 added dependency caveat oheimb parents: 9276 diff changeset	2	ID: $Id$
a0a7c31cdc39 added dependency caveat oheimb parents: 9276 diff changeset	3	Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
a0a7c31cdc39 added dependency caveat oheimb parents: 9276 diff changeset	4	Copyright 1995 TUM
9276 9e619ac0fe2f added dependency caveat oheimb parents: 9241 diff changeset	5
9e619ac0fe2f added dependency caveat oheimb parents: 9241 diff changeset	6	Caveat: HOLCF/IMP depends on HOL/IMP
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	7	*)
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	8
1696 e84bff5c519b A completely new version of IMP. nipkow parents: 1465 diff changeset	9	time_use_thy "Expr";
e84bff5c519b A completely new version of IMP. nipkow parents: 1465 diff changeset	10	time_use_thy "Transition";
1447 bc2c0acbbf29 Added a verified verification-condition generator. nipkow parents: 1351 diff changeset	11	time_use_thy "VC";
9241 f961c1fdff50 disambiguated := ; added Examples (factorial) oheimb parents: 9000 diff changeset	12	time_use_thy "Examples";
13095 8ed413a57bdc New machine architecture and other direction of compiler proof. nipkow parents: 10342 diff changeset	13	time_use_thy "Compiler0";
10342 b124d59f7b61 * empty log message * nipkow parents: 9277 diff changeset	14	time_use_thy "Compiler";

author	ballarin
	Wed, 19 Jul 2006 19:25:58 +0200
changeset 20168	ed7bced29e1b
parent 13095	8ed413a57bdc
child 24104	719fbe4fb77f
permissions	-rw-r--r--