--- a/src/HOL/Main.thy Sat Sep 17 18:11:20 2005 +0200
+++ b/src/HOL/Main.thy Sat Sep 17 18:11:21 2005 +0200
@@ -1,14 +1,9 @@
-(* Title: HOL/Main.thy
- ID: $Id$
- Author: Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
-*)
+(* $Id$ *)
header {* Main HOL *}
theory Main
-imports Refute Reconstruction
- (*other theores need to be ancestors of Reconstruction, not Main!!*)
-
+imports Refute Reconstruction
begin
text {*
@@ -17,9 +12,10 @@
*}
-subsection {* Misc *}
+subsection {* Special hacks, late package setup etc. *}
-text {* Hide the rather generic names used in theory @{text Commutative_Ring}. *}
+text {* \medskip Hide the rather generic names used in theory @{text
+ Commutative_Ring}. *}
hide (open) const
Pc Pinj PX
@@ -28,74 +24,23 @@
norm
-subsection {* Configuration of the code generator *}
-
-types_code
- "bool" ("bool")
-attach (term_of) {*
-fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
-*}
-attach (test) {*
-fun gen_bool i = one_of [false, true];
-*}
-
-consts_code
- "True" ("true")
- "False" ("false")
- "Not" ("not")
- "op |" ("(_ orelse/ _)")
- "op &" ("(_ andalso/ _)")
- "HOL.If" ("(if _/ then _/ else _)")
-
- "wfrec" ("\<module>wf'_rec?")
-attach {*
-fun wf_rec f x = f (wf_rec f) x;
+text {* \medskip Default values for rufute, see also theory @{text
+ Refute}.
*}
-quickcheck_params [default_type = int]
-
-ML {*
-local
-
-fun eq_codegen thy defs gr dep thyname b t =
- (case strip_comb t of
- (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
- | (Const ("op =", _), [t, u]) =>
- let
- val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
- val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
- in
- SOME (gr'', Codegen.parens
- (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
- end
- | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
- thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
- | _ => NONE);
-
-in
-
-val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
-
-end;
-*}
-
-setup eq_codegen_setup
-
-lemmas [code] = imp_conv_disj
+refute_params
+ ["itself"=1,
+ minsize=1,
+ maxsize=8,
+ maxvars=10000,
+ maxtime=60,
+ satsolver="auto"]
-subsection {* Configuration of the 'refute' command *}
-
-text {*
- The following are fairly reasonable default values. For an
- explanation of these parameters, see 'HOL/Refute.thy'.
-*}
+text {* \medskip Clause setup: installs \emph{all} simprules and
+ claset rules into the clause cache; cf.\ theory @{text
+ Reconstruction}. *}
-refute_params ["itself"=1,
- minsize=1,
- maxsize=8,
- maxvars=10000,
- maxtime=60,
- satsolver="auto"]
+setup ResAxioms.clause_setup
end