isabelle: src/HOL/Main.thy@93d0f85cfe4a (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
42695 a94ad372b2f5 adding creation of exhaustive generators for records; simplifying dependencies in Main theory bulwahn parents: 41919 diff changeset	4	imports Plain Predicate_Compile Nitpick
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
44324 d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	14	text {* Compatibility layer -- to be dropped *}
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	15
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	16	lemma Inf_bool_def:
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	17	"Inf A \<longleftrightarrow> (\<forall>x\<in>A. x)"
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	18	by (auto intro: bool_induct)
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	19
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	20	lemma Sup_bool_def:
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	21	"Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	22	by auto
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	23
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	24	declare Complete_Lattice.Inf_bool_def [simp del]
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	25	declare Complete_Lattice.Sup_bool_def [simp del]
d972b91ed09d compatibility layer haftmann parents: 42695 diff changeset	26
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	27	end

author	huffman
	Thu, 08 Sep 2011 07:27:57 -0700
changeset 44843	93d0f85cfe4a
parent 44324	d972b91ed09d
child 44860	56101fa00193
permissions	-rw-r--r--