isabelle: src/HOL/Main.thy@4e700eb471d4 (annotated)

12024 b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	1	header {* Main HOL *}
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	2
15131 c69542757a4d New theory header syntax. nipkow parents: 15063 diff changeset	3	theory Main
55058 4e700eb471d4 moved BNF files to 'HOL' blanchet parents: 55057 diff changeset	4	imports Predicate_Compile Nitpick Extraction Lifting_Sum List_Prefix Coinduction BNF_LFP BNF_GFP
15131 c69542757a4d New theory header syntax. nipkow parents: 15063 diff changeset	5	begin
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	6
29304 5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	7	text {*
5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	8	Classical Higher-order Logic -- only ``Main'', excluding real and
5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	9	complex numbers etc.
5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	10	*}
5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	11
27367 a75d71c73362 added dummy citiation haftmann parents: 26729 diff changeset	12	text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
25964 080f89d89990 consistent interacitve bootstrap of HOL-Main haftmann parents: 25223 diff changeset	13
51112 da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	14	no_notation
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	15	bot ("\<bottom>") and
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	16	top ("\<top>") and
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	17	inf (infixl "\<sqinter>" 70) and
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	18	sup (infixl "\<squnion>" 65) and
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	19	Inf ("\<Sqinter>_" [900] 900) and
55057 6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	20	Sup ("\<Squnion>_" [900] 900) and
6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	21	ordLeq2 ("<=o") and
6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	22	ordLeq3 ("\<le>o") and
6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	23	ordLess2 ("<o") and
6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	24	ordIso2 ("=o") and
6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	25	csum (infixr "+c" 65) and
6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	26	cprod (infixr "*c" 80) and
6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	27	cexp (infixr "^c" 90)
51112 da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	28
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	29	no_syntax (xsymbols)
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	30	"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	31	"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	32	"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	33	"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	34
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	35	end

author	blanchet
	Mon, 20 Jan 2014 18:24:56 +0100
changeset 55058	4e700eb471d4
parent 55057	6b0fcbeebaba
child 55062	6d3fad6f01c9
permissions	-rw-r--r--