src/HOL/Main.thy
author haftmann
Tue, 09 May 2006 14:18:40 +0200
changeset 19607 07eeb832f28d
parent 18510 0a6c24f549c3
child 19608 81fe44909dd5
permissions -rw-r--r--
introduced characters for code generator; some improved code lemmas for some list functions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17602
63367feba417 header (title/ID) added
webertj
parents: 17601
diff changeset
     1
(*  Title:      HOL/Main.thy
63367feba417 header (title/ID) added
webertj
parents: 17601
diff changeset
     2
    ID:         $Id$
63367feba417 header (title/ID) added
webertj
parents: 17601
diff changeset
     3
*)
9619
6125cc9efc18 fixed deps;
wenzelm
parents: 9447
diff changeset
     4
12024
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     5
header {* Main HOL *}
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
     6
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
     7
theory Main
17905
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents: 17721
diff changeset
     8
imports SAT Reconstruction ResAtpMethods
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15063
diff changeset
     9
begin
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    10
12024
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    11
text {*
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    12
  Theory @{text Main} includes everything.  Note that theory @{text
b3661262541e moved String into Main;
wenzelm
parents: 11533
diff changeset
    13
  PreList} already includes most HOL theories.
17395
a05e20f6a31a hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents: 17386
diff changeset
    14
17721
b943c01e1c6d explicit dependencies of SAT vs. Refute;
wenzelm
parents: 17618
diff changeset
    15
text {* \medskip Late clause setup: installs \emph{all} simprules and
17461
83f1dd9d901d minor cleanup, moved stuff in its proper place;
wenzelm
parents: 17421
diff changeset
    16
  claset rules into the clause cache; cf.\ theory @{text
83f1dd9d901d minor cleanup, moved stuff in its proper place;
wenzelm
parents: 17421
diff changeset
    17
  Reconstruction}. *}
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
    18
18510
0a6c24f549c3 the "skolem" attribute and better initialization of the clause database
paulson
parents: 18315
diff changeset
    19
setup ResAxioms.setup
14350
41b32020d0b3 Adding 'refute' to HOL.
webertj
parents: 14192
diff changeset
    20
9650
6f0b89f2a1f9 Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents: 9619
diff changeset
    21
end