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