isabelle: src/HOL/Plain.thy@eb7a797ade0f (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	end