isabelle: src/HOL/Main.thy@66ef82187de1 (annotated)

17602 63367feba417 header (title/ID) added webertj parents: 17601 diff changeset	1	(* Title: HOL/Main.thy
63367feba417 header (title/ID) added webertj parents: 17601 diff changeset	2	ID: $Id$
63367feba417 header (title/ID) added webertj parents: 17601 diff changeset	3	*)
9619 6125cc9efc18 fixed deps; wenzelm parents: 9447 diff changeset	4
12024 b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	5	header {* Main HOL *}
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	6
15131 c69542757a4d New theory header syntax. nipkow parents: 15063 diff changeset	7	theory Main
24632 779fc4fcbf8b metis now available in PreList paulson parents: 23165 diff changeset	8	imports Map
15131 c69542757a4d New theory header syntax. nipkow parents: 15063 diff changeset	9	begin
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	10
12024 b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	11	text {*
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	12	Theory @{text Main} includes everything. Note that theory @{text
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	13	PreList} already includes most HOL theories.
22840 643bb625a2c3 minimal import haftmann parents: 21254 diff changeset	14
643bb625a2c3 minimal import haftmann parents: 21254 diff changeset	15	\medskip Late clause setup: installs \emph{all} known theorems
24632 779fc4fcbf8b metis now available in PreList paulson parents: 23165 diff changeset	16	into the clause cache; cf.\ theory @{text ATP_Linkup}.
24644 66ef82187de1 Enclosed end_theory in text antiquotation to make LaTeX happy. berghofe parents: 24632 diff changeset	17	FIXME: delete once @{text end_theory} actions are installed!
19608 81fe44909dd5 revert accidental text change; wenzelm parents: 19607 diff changeset	18	*}
17395 a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	19
24632 779fc4fcbf8b metis now available in PreList paulson parents: 23165 diff changeset	20	setup ResAxioms.clause_cache_setup
14350 41b32020d0b3 Adding 'refute' to HOL. webertj parents: 14192 diff changeset	21
23165 5d319b0f8bf9 HOL_proofs; wenzelm parents: 22840 diff changeset	22	ML {* val HOL_proofs = !proofs *}
5d319b0f8bf9 HOL_proofs; wenzelm parents: 22840 diff changeset	23
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	24	end

author	berghofe
	Wed, 19 Sep 2007 12:17:13 +0200
changeset 24644	66ef82187de1
parent 24632	779fc4fcbf8b
child 24699	c6674504103f
permissions	-rw-r--r--