isabelle: src/HOL/Main.thy@2db1df2c8467 (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
58128 43a1ba26a8cb renamed BNF theories blanchet parents: 58055 diff changeset	4	imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
58377 c6f93b8d2d8e moved old 'size' generator together with 'old_datatype' blanchet parents: 58372 diff changeset	5	BNF_Greatest_Fixpoint
15131 c69542757a4d New theory header syntax. nipkow parents: 15063 diff changeset	6	begin
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	7
29304 5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	8	text {*
5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	9	Classical Higher-order Logic -- only ``Main'', excluding real and
5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	10	complex numbers etc.
5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	11	*}
5c71a6da989d tuned header and description of boot files; wenzelm parents: 28263 diff changeset	12
58623 2db1df2c8467 more bibtex entries; wenzelm parents: 58377 diff changeset	13	text {* See further @{cite "Nipkow-et-al:2002:tutorial"} *}
25964 080f89d89990 consistent interacitve bootstrap of HOL-Main haftmann parents: 25223 diff changeset	14
51112 da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	15	no_notation
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	16	bot ("\<bottom>") and
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	17	top ("\<top>") and
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	18	inf (infixl "\<sqinter>" 70) and
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	19	sup (infixl "\<squnion>" 65) and
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	20	Inf ("\<Sqinter>_" [900] 900) and
55057 6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	21	Sup ("\<Squnion>_" [900] 900) and
55065 6d0af3c10864 compile blanchet parents: 55062 diff changeset	22	ordLeq2 (infix "<=o" 50) and
6d0af3c10864 compile blanchet parents: 55062 diff changeset	23	ordLeq3 (infix "\<le>o" 50) and
6d0af3c10864 compile blanchet parents: 55062 diff changeset	24	ordLess2 (infix "<o" 50) and
6d0af3c10864 compile blanchet parents: 55062 diff changeset	25	ordIso2 (infix "=o" 50) and
55078 558c9ceabaa1 deactivate one more cardinal notation blanchet parents: 55069 diff changeset	26	card_of ("\|_\|") and
55057 6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	27	csum (infixr "+c" 65) and
6b0fcbeebaba kill notations blanchet parents: 55056 diff changeset	28	cprod (infixr "*c" 80) and
55086 500ef036117b hide BNF notation blanchet parents: 55079 diff changeset	29	cexp (infixr "^c" 90) and
57641 dc59f147b27d more robust notation BNF_Def.convol, which is private to main HOL, but may cause syntax ambiguities nonetheless (e.g. List.thy); wenzelm parents: 57208 diff changeset	30	convol ("\<langle>(_,/ _)\<rangle>")
51112 da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	31
55087 252c7fec4119 renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test) blanchet parents: 55086 diff changeset	32	hide_const (open)
58152 6fe60a9a5bad use 'datatype_new' in 'Main' blanchet parents: 58128 diff changeset	33	czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
6fe60a9a5bad use 'datatype_new' in 'Main' blanchet parents: 58128 diff changeset	34	fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
58353 c9f374b64d99 tuned fact visibility blanchet parents: 58352 diff changeset	35	shift proj id_bnf
c9f374b64d99 tuned fact visibility blanchet parents: 58352 diff changeset	36
c9f374b64d99 tuned fact visibility blanchet parents: 58352 diff changeset	37	hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
55087 252c7fec4119 renamed 'regular' to 'regularCard' to avoid clashes (e.g. in Meson_Test) blanchet parents: 55086 diff changeset	38
51112 da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	39	no_syntax (xsymbols)
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	40	"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10)
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	41	"_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	42	"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
da97167e03f7 abandoned theory Plain haftmann parents: 46155 diff changeset	43	"_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	44
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	45	end

author	wenzelm
	Tue, 07 Oct 2014 23:29:43 +0200
changeset 58623	2db1df2c8467
parent 58377	c6f93b8d2d8e
child 58770	ae5e9b4f8daf
permissions	-rw-r--r--