isabelle: src/HOL/Plain.thy@62da280e5d0b (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
29820 07f53494cf20 Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML + blanchet parents: 29609 diff changeset	4	imports Datatype FunDef Record Extraction Divides
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
29609 a010aab5bed0 changed import hierarchy haftmann parents: 29304 diff changeset	12	instance option :: (finite) finite
a010aab5bed0 changed import hierarchy haftmann parents: 29304 diff changeset	13	by default (simp add: insert_None_conv_UNIV [symmetric])
a010aab5bed0 changed import hierarchy haftmann parents: 29304 diff changeset	14
27368 9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	15	ML {* path_add "~~/src/HOL/Library" *}
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	16
9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	17	end

author	chaieb
	Mon, 09 Feb 2009 11:07:17 +0000
changeset 29835	62da280e5d0b
parent 29820	07f53494cf20
child 29837	eb7e62c0f53c
permissions	-rw-r--r--