isabelle: src/HOL/Main.thy@83f1dd9d901d (annotated)

17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	1	(* $Id$ *)
9619 6125cc9efc18 fixed deps; wenzelm parents: 9447 diff changeset	2
12024 b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	3	header {* Main HOL *}
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	4
15131 c69542757a4d New theory header syntax. nipkow parents: 15063 diff changeset	5	theory Main
17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	6	imports Refute Reconstruction
15131 c69542757a4d New theory header syntax. nipkow parents: 15063 diff changeset	7	begin
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	8
12024 b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	9	text {*
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	10	Theory @{text Main} includes everything. Note that theory @{text
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	11	PreList} already includes most HOL theories.
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	12	*}
b3661262541e moved String into Main; wenzelm parents: 11533 diff changeset	13
17395 a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	14
17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	15	subsection {* Special hacks, late package setup etc. *}
17395 a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	16
17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	17	text {* \medskip Hide the rather generic names used in theory @{text
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	18	Commutative_Ring}. *}
17395 a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	19
a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	20	hide (open) const
a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	21	Pc Pinj PX
a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	22	Pol Add Sub Mul Pow Neg
a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	23	add mul neg sqr pow sub
a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	24	norm
a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	25
a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	26
17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	27	text {* \medskip Default values for rufute, see also theory @{text
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	28	Refute}.
16770 1f1b1fae30e4 Auxiliary functions to be used in generated code are now defined using "attach". berghofe parents: 16635 diff changeset	29	*}
13093 ab0335307905 code generator: wfrec combinator is now implemented by ML function wf_rec. berghofe parents: 12554 diff changeset	30
17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	31	refute_params
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	32	["itself"=1,
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	33	minsize=1,
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	34	maxsize=8,
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	35	maxvars=10000,
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	36	maxtime=60,
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	37	satsolver="auto"]
12554 671b4d632c34 Declared characteristic equations for < on nat for code generation. berghofe parents: 12439 diff changeset	38
17395 a05e20f6a31a hide the rather generic names used in theory Commutative_Ring; wenzelm parents: 17386 diff changeset	39
17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	40	text {* \medskip Clause setup: installs \emph{all} simprules and
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	41	claset rules into the clause cache; cf.\ theory @{text
83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	42	Reconstruction}. *}
14350 41b32020d0b3 Adding 'refute' to HOL. webertj parents: 14192 diff changeset	43
17461 83f1dd9d901d minor cleanup, moved stuff in its proper place; wenzelm parents: 17421 diff changeset	44	setup ResAxioms.clause_setup
14350 41b32020d0b3 Adding 'refute' to HOL. webertj parents: 14192 diff changeset	45
9650 6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility; wenzelm parents: 9619 diff changeset	46	end

author	wenzelm
	Sat, 17 Sep 2005 18:11:21 +0200
changeset 17461	83f1dd9d901d
parent 17421	0382f6877b98
child 17509	054cd8972095
permissions	-rw-r--r--