isabelle: src/HOL/Plain.thy@a45e8c872dc1 (annotated)

27368 9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	1	(* Title: HOL/Plain.thy
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	Contains fundamental HOL tools and packages. Does not include Hilbert_Choice.
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	header {* Plain HOL *}
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	8
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	9	theory Plain
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	10	imports Datatype FunDef Record SAT Extraction
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	11	begin
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	12
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	13	ML {* path_add "~~/src/HOL/Library" *}
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	14
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	15	end

author	nipkow
	Mon, 01 Sep 2008 22:10:42 +0200
changeset 28072	a45e8c872dc1
parent 27368	9f90ac19e32b
child 29304	5c71a6da989d
permissions	-rw-r--r--