# HG changeset patch
# User wenzelm
# Date 1126973481 -7200
# Node ID 83f1dd9d901da2bcdf0127e7b47bbf12d983ef1f
# Parent  7780d953598c92d69105a7b1c249692203051977
minor cleanup, moved stuff in its proper place;

diff -r 7780d953598c -r 83f1dd9d901d src/HOL/Main.thy
--- 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