isabelle: src/HOL/IMP/ROOT.ML@719fbe4fb77f (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
24104 719fbe4fb77f simultaneous use_thys; wenzelm parents: 13095 diff changeset	9	use_thys ["Expr", "Transition", "VC", "Examples", "Compiler0", "Compiler"];