isabelle: src/HOL/IMP/ROOT.ML@d8efc2490b8e (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	Author: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow, David von Oheimb
9276 9e619ac0fe2f added dependency caveat oheimb parents: 9241 diff changeset	3
9e619ac0fe2f added dependency caveat oheimb parents: 9241 diff changeset	4	Caveat: HOLCF/IMP depends on HOL/IMP
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
35754 8e7dba5f00f5 Reorganized Hoare logic theories; added Hoare_Den nipkow parents: 35749 diff changeset	7	use_thys ["Expr", "Transition", "VC", "Hoare_Den", "Examples", "Compiler0", "Compiler", "Live"];