isabelle: src/HOL/Main.thy@e52f867ab851 (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
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: 17721 diff changeset	8	imports SAT Reconstruction ResAtpMethods
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.
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	14	*}
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	15
17395 a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	16
17721 b943c01e1c6d explicit dependencies of SAT vs. Refute; wenzelm parents: 17618 diff changeset	17	text {* \medskip Late clause setup: installs \emph{all} simprules and
17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	18	claset rules into the clause cache; cf.\ theory @{text
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	19	Reconstruction}. *}
14350 41b32020d0b3 Adding 'refute' to HOL. webertj parents: 14192 diff changeset	20
18315 e52f867ab851 restoring the old status of subset_refl paulson parents: 17905 diff changeset	21	declare subset_refl [intro]
e52f867ab851 restoring the old status of subset_refl paulson parents: 17905 diff changeset	22	text {*Ensures that this important theorem is not superseded by the
e52f867ab851 restoring the old status of subset_refl paulson parents: 17905 diff changeset	23	simplifier's "== True" version.*}
17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	24	setup ResAxioms.clause_setup
18315 e52f867ab851 restoring the old status of subset_refl paulson parents: 17905 diff changeset	25	declare subset_refl [rule del]
e52f867ab851 restoring the old status of subset_refl paulson parents: 17905 diff changeset	26	text {Removed again because it harms blast's performance.}
14350 41b32020d0b3 Adding 'refute' to HOL. webertj parents: 14192 diff changeset	27
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	28	end

author	paulson
	Thu, 01 Dec 2005 15:45:54 +0100
changeset 18315	e52f867ab851
parent 17905	1574533861b1
child 18510	0a6c24f549c3
permissions	-rw-r--r--