Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Main.thy
author paulson
Fri, 23 Dec 2005 17:37:54 +0100
changeset 18510 0a6c24f549c3
parent 18315 e52f867ab851
child 19607 07eeb832f28d
permissions -rw-r--r--
the "skolem" attribute and better initialization of the clause database
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.













b3661262541e
moved String into Main;



wenzelm


parents: 
11533

diff
changeset




    14


*}













b3661262541e
moved String into Main;



wenzelm


parents: 
11533

diff
changeset




    15









17395






a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;



wenzelm


parents: 
17386

diff
changeset




    16









17721






b943c01e1c6d
explicit dependencies of SAT vs. Refute;



wenzelm


parents: 
17618

diff
changeset




    17


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




    18


  claset rules into the clause cache; cf.\ theory @{text













83f1dd9d901d
minor cleanup, moved stuff in its proper place;



wenzelm


parents: 
17421

diff
changeset




    19


  Reconstruction}. *}








14350






41b32020d0b3
Adding 'refute' to HOL.



webertj


parents: 
14192

diff
changeset




    20









18510






0a6c24f549c3
the "skolem" attribute and better initialization of the clause database



paulson


parents: 
18315

diff
changeset




    21


setup ResAxioms.setup








14350






41b32020d0b3
Adding 'refute' to HOL.



webertj


parents: 
14192

diff
changeset




    22









9650






6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;



wenzelm


parents: 
9619

diff
changeset




    23


end















isabelle