isabelle: src/HOL/plain.ML@a45e8c872dc1 (annotated)

27368 9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	1	(* Title: HOL/plain.ML
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	2	ID: $Id$
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	3
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	4	Classical Higher-order Logic -- plain Tool bootstrap.
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	5	*)
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	6
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	7	use_thy "Plain";