isabelle: src/HOL/Plain.thy@cd1fcda1ea88 (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
47108 2a1953f0d20d merged fork with new numeral representation (see NEWS) huffman parents: 46691 diff changeset	4	imports Datatype FunDef Extraction Metis Num
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
46691 72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	12	no_notation
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	13	bot ("\<bottom>") and
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	14	top ("\<top>") and
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	15	inf (infixl "\<sqinter>" 70) and
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	16	sup (infixl "\<squnion>" 65) and
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	17	Inf ("\<Sqinter>_" [900] 900) and
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	18	Sup ("\<Squnion>_" [900] 900)
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	19
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	20	no_syntax (xsymbols)
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	21	"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	22	"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	23	"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	24	"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
72d81e789106 tuned syntax declarations; tuned structure haftmann parents: 41886 diff changeset	25
27368 9f90ac19e32b established Plain theory and image haftmann parents: diff changeset	26	end

author	blanchet
	Thu, 03 Jan 2013 17:10:12 +0100
changeset 50704	cd1fcda1ea88
parent 47108	2a1953f0d20d
permissions	-rw-r--r--