author | webertj |
Fri, 23 Sep 2005 16:01:45 +0200 | |
changeset 17602 | 63367feba417 |
parent 17601 | a6a322f96145 |
child 17618 | 1330157e156a |
permissions | -rw-r--r-- |
17602 | 1 |
(* Title: HOL/Main.thy |
2 |
ID: $Id$ |
|
3 |
*) |
|
9619 | 4 |
|
12024 | 5 |
header {* Main HOL *} |
6 |
||
15131 | 7 |
theory Main |
17461 | 8 |
imports Refute Reconstruction |
15131 | 9 |
begin |
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
10 |
|
12024 | 11 |
text {* |
12 |
Theory @{text Main} includes everything. Note that theory @{text |
|
13 |
PreList} already includes most HOL theories. |
|
14 |
*} |
|
15 |
||
17395
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
16 |
|
17461 | 17 |
subsection {* Special hacks, late package setup etc. *} |
17395
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
18 |
|
17601 | 19 |
text {* \medskip Default values for refute, see also theory @{text |
17461 | 20 |
Refute}. |
16770
1f1b1fae30e4
Auxiliary functions to be used in generated code are now defined using "attach".
berghofe
parents:
16635
diff
changeset
|
21 |
*} |
13093
ab0335307905
code generator: wfrec combinator is now implemented by ML function wf_rec.
berghofe
parents:
12554
diff
changeset
|
22 |
|
17461 | 23 |
refute_params |
24 |
["itself"=1, |
|
25 |
minsize=1, |
|
26 |
maxsize=8, |
|
27 |
maxvars=10000, |
|
28 |
maxtime=60, |
|
29 |
satsolver="auto"] |
|
12554
671b4d632c34
Declared characteristic equations for < on nat for code generation.
berghofe
parents:
12439
diff
changeset
|
30 |
|
17395
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
31 |
|
17461 | 32 |
text {* \medskip Clause setup: installs \emph{all} simprules and |
33 |
claset rules into the clause cache; cf.\ theory @{text |
|
34 |
Reconstruction}. *} |
|
14350 | 35 |
|
17461 | 36 |
setup ResAxioms.clause_setup |
14350 | 37 |
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
38 |
end |