src/HOL/Main.thy
author webertj
Fri Sep 23 15:45:12 2005 +0200 (2005-09-23)
changeset 17601 a6a322f96145
parent 17509 054cd8972095
child 17602 63367feba417
permissions -rw-r--r--
typo fixed: rufute -> refute
wenzelm@17461
     1
(* $Id$ *)
wenzelm@9619
     2
wenzelm@12024
     3
header {* Main HOL *}
wenzelm@12024
     4
nipkow@15131
     5
theory Main
wenzelm@17461
     6
imports Refute Reconstruction
nipkow@15131
     7
begin
wenzelm@9650
     8
wenzelm@12024
     9
text {*
wenzelm@12024
    10
  Theory @{text Main} includes everything.  Note that theory @{text
wenzelm@12024
    11
  PreList} already includes most HOL theories.
wenzelm@12024
    12
*}
wenzelm@12024
    13
wenzelm@17395
    14
wenzelm@17461
    15
subsection {* Special hacks, late package setup etc. *}
wenzelm@17395
    16
webertj@17601
    17
text {* \medskip Default values for refute, see also theory @{text
wenzelm@17461
    18
  Refute}.
berghofe@16770
    19
*}
berghofe@13093
    20
wenzelm@17461
    21
refute_params
wenzelm@17461
    22
 ["itself"=1,
wenzelm@17461
    23
  minsize=1,
wenzelm@17461
    24
  maxsize=8,
wenzelm@17461
    25
  maxvars=10000,
wenzelm@17461
    26
  maxtime=60,
wenzelm@17461
    27
  satsolver="auto"]
berghofe@12554
    28
wenzelm@17395
    29
wenzelm@17461
    30
text {* \medskip Clause setup: installs \emph{all} simprules and
wenzelm@17461
    31
  claset rules into the clause cache; cf.\ theory @{text
wenzelm@17461
    32
  Reconstruction}. *}
webertj@14350
    33
wenzelm@17461
    34
setup ResAxioms.clause_setup
webertj@14350
    35
wenzelm@9650
    36
end