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

27368 9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	1	header {* Plain HOL *}
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	2
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	3	theory Plain
40178 00152d17855b reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers blanchet parents: 40121 diff changeset	4	imports Datatype FunDef Extraction Metis
27368 9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	5	begin
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	6
29304 5c71a6da989d tuned header and description of boot files; wenzelm parents: 27368 diff changeset	7	text {*
5c71a6da989d tuned header and description of boot files; wenzelm parents: 27368 diff changeset	8	Plain bootstrap of fundamental HOL tools and packages; does not
5c71a6da989d tuned header and description of boot files; wenzelm parents: 27368 diff changeset	9	include @{text Hilbert_Choice}.
5c71a6da989d tuned header and description of boot files; wenzelm parents: 27368 diff changeset	10	*}
5c71a6da989d tuned header and description of boot files; wenzelm parents: 27368 diff changeset	11
27368 9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	12	ML {* path_add "~~/src/HOL/Library" *}
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	13
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	14	end

author	wenzelm
	Sat, 27 Nov 2010 11:51:05 +0100
changeset 40739	9c84b562620d
parent 40178	00152d17855b
child 41414	00b2b6716ed8
permissions	-rw-r--r--