isabelle: src/HOL/IMP/ROOT.ML@61dd8c145da7 (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
35754 8e7dba5f00f5 Reorganized Hoare logic theories; added Hoare_Den nipkow parents: 35749 diff changeset	9	use_thys ["Expr", "Transition", "VC", "Hoare_Den", "Examples", "Compiler0", "Compiler", "Live"];