isabelle: src/HOL/Plain.thy@5bdcdb28be83 (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
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	huffman
	Fri, 16 Mar 2012 15:51:53 +0100
changeset 46962	5bdcdb28be83
parent 46691	72d81e789106
child 47108	2a1953f0d20d
permissions	-rw-r--r--