isabelle: src/HOL/Plain.thy@1ebc6b76e5ff (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
38393 7c045c03598f group record-related ML files haftmann parents: 33593 diff changeset	4	imports Datatype FunDef Extraction
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
	Sun, 22 Aug 2010 19:33:01 +0200
changeset 38578	1ebc6b76e5ff
parent 38393	7c045c03598f
child 39941	02fcd9cd1eac
permissions	-rw-r--r--