src/HOL/Main.thy
changeset 17461 83f1dd9d901d
parent 17421 0382f6877b98
child 17509 054cd8972095
     1.1 --- a/src/HOL/Main.thy	Sat Sep 17 18:11:20 2005 +0200
     1.2 +++ b/src/HOL/Main.thy	Sat Sep 17 18:11:21 2005 +0200
     1.3 @@ -1,14 +1,9 @@
     1.4 -(*  Title:      HOL/Main.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Stefan Berghofer, Tobias Nipkow, Tjark Weber, Markus Wenzel (TU Muenchen)
     1.7 -*)
     1.8 +(* $Id$ *)
     1.9  
    1.10  header {* Main HOL *}
    1.11  
    1.12  theory Main
    1.13 -imports Refute Reconstruction 
    1.14 -        (*other theores need to be ancestors of Reconstruction, not Main!!*)
    1.15 -
    1.16 +imports Refute Reconstruction
    1.17  begin
    1.18  
    1.19  text {*
    1.20 @@ -17,9 +12,10 @@
    1.21  *}
    1.22  
    1.23  
    1.24 -subsection {* Misc *}
    1.25 +subsection {* Special hacks, late package setup etc. *}
    1.26  
    1.27 -text {* Hide the rather generic names used in theory @{text Commutative_Ring}. *}
    1.28 +text {* \medskip Hide the rather generic names used in theory @{text
    1.29 +  Commutative_Ring}. *}
    1.30  
    1.31  hide (open) const
    1.32    Pc Pinj PX
    1.33 @@ -28,74 +24,23 @@
    1.34    norm
    1.35  
    1.36  
    1.37 -subsection {* Configuration of the code generator *}
    1.38 -
    1.39 -types_code
    1.40 -  "bool"  ("bool")
    1.41 -attach (term_of) {*
    1.42 -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.43 -*}
    1.44 -attach (test) {*
    1.45 -fun gen_bool i = one_of [false, true];
    1.46 -*}
    1.47 -
    1.48 -consts_code
    1.49 -  "True"    ("true")
    1.50 -  "False"   ("false")
    1.51 -  "Not"     ("not")
    1.52 -  "op |"    ("(_ orelse/ _)")
    1.53 -  "op &"    ("(_ andalso/ _)")
    1.54 -  "HOL.If"      ("(if _/ then _/ else _)")
    1.55 -
    1.56 -  "wfrec"   ("\<module>wf'_rec?")
    1.57 -attach {*
    1.58 -fun wf_rec f x = f (wf_rec f) x;
    1.59 +text {* \medskip Default values for rufute, see also theory @{text
    1.60 +  Refute}.
    1.61  *}
    1.62  
    1.63 -quickcheck_params [default_type = int]
    1.64 -
    1.65 -ML {*
    1.66 -local
    1.67 -
    1.68 -fun eq_codegen thy defs gr dep thyname b t =
    1.69 -    (case strip_comb t of
    1.70 -       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    1.71 -     | (Const ("op =", _), [t, u]) =>
    1.72 -          let
    1.73 -            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    1.74 -            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u)
    1.75 -          in
    1.76 -            SOME (gr'', Codegen.parens
    1.77 -              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    1.78 -          end
    1.79 -     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    1.80 -         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    1.81 -     | _ => NONE);
    1.82 -
    1.83 -in
    1.84 -
    1.85 -val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
    1.86 -
    1.87 -end;
    1.88 -*}
    1.89 -
    1.90 -setup eq_codegen_setup
    1.91 -
    1.92 -lemmas [code] = imp_conv_disj
    1.93 +refute_params
    1.94 + ["itself"=1,
    1.95 +  minsize=1,
    1.96 +  maxsize=8,
    1.97 +  maxvars=10000,
    1.98 +  maxtime=60,
    1.99 +  satsolver="auto"]
   1.100  
   1.101  
   1.102 -subsection {* Configuration of the 'refute' command *}
   1.103 -
   1.104 -text {*
   1.105 -  The following are fairly reasonable default values.  For an
   1.106 -  explanation of these parameters, see 'HOL/Refute.thy'.
   1.107 -*}
   1.108 +text {* \medskip Clause setup: installs \emph{all} simprules and
   1.109 +  claset rules into the clause cache; cf.\ theory @{text
   1.110 +  Reconstruction}. *}
   1.111  
   1.112 -refute_params ["itself"=1,
   1.113 -               minsize=1,
   1.114 -               maxsize=8,
   1.115 -               maxvars=10000,
   1.116 -               maxtime=60,
   1.117 -               satsolver="auto"]
   1.118 +setup ResAxioms.clause_setup
   1.119  
   1.120  end