src/HOL/Main.thy
author wenzelm
Sat Sep 17 18:11:21 2005 +0200 (2005-09-17)
changeset 17461 83f1dd9d901d
parent 17421 0382f6877b98
child 17509 054cd8972095
permissions -rw-r--r--
minor cleanup, moved stuff in its proper place;
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
wenzelm@17461
    17
text {* \medskip Hide the rather generic names used in theory @{text
wenzelm@17461
    18
  Commutative_Ring}. *}
wenzelm@17395
    19
wenzelm@17395
    20
hide (open) const
wenzelm@17395
    21
  Pc Pinj PX
wenzelm@17395
    22
  Pol Add Sub Mul Pow Neg
wenzelm@17395
    23
  add mul neg sqr pow sub
wenzelm@17395
    24
  norm
wenzelm@17395
    25
wenzelm@17395
    26
wenzelm@17461
    27
text {* \medskip Default values for rufute, see also theory @{text
wenzelm@17461
    28
  Refute}.
berghofe@16770
    29
*}
berghofe@13093
    30
wenzelm@17461
    31
refute_params
wenzelm@17461
    32
 ["itself"=1,
wenzelm@17461
    33
  minsize=1,
wenzelm@17461
    34
  maxsize=8,
wenzelm@17461
    35
  maxvars=10000,
wenzelm@17461
    36
  maxtime=60,
wenzelm@17461
    37
  satsolver="auto"]
berghofe@12554
    38
wenzelm@17395
    39
wenzelm@17461
    40
text {* \medskip Clause setup: installs \emph{all} simprules and
wenzelm@17461
    41
  claset rules into the clause cache; cf.\ theory @{text
wenzelm@17461
    42
  Reconstruction}. *}
webertj@14350
    43
wenzelm@17461
    44
setup ResAxioms.clause_setup
webertj@14350
    45
wenzelm@9650
    46
end