2005-09-21 |
paulson |
improved proof parsing
|
file |
diff |
annotate
|
2005-09-19 |
paulson |
further simplification of the Isabelle-ATP linkup
|
file |
diff |
annotate
|
2005-09-19 |
paulson |
simplification of the Isabelle-ATP code; hooks for batch generation of problems
|
file |
diff |
annotate
|
2005-09-15 |
paulson |
massive tidy-up and simplification
|
file |
diff |
annotate
|
2005-09-09 |
paulson |
Isabelle-ATP link: sortable axiom names; no spaces in switches; general tidying
|
file |
diff |
annotate
|
2005-09-08 |
paulson |
consolidation of duplicate code in Isabelle-ATP linkup
|
file |
diff |
annotate
|
2005-09-08 |
paulson |
yet more tidying of Isabelle-ATP link
|
file |
diff |
annotate
|
2005-09-07 |
paulson |
Progress on eprover linkup, also massive tidying
|
file |
diff |
annotate
|
2005-09-02 |
quigley |
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
|
file |
diff |
annotate
|
2005-08-18 |
paulson |
nicer list of axioms used
|
file |
diff |
annotate
|
2005-07-22 |
paulson |
reformatting and tidying
|
file |
diff |
annotate
|
2005-07-13 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2005-06-22 |
quigley |
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
|
file |
diff |
annotate
|
2005-06-21 |
quigley |
Integrated vampire lemma code.
|
file |
diff |
annotate
|
2005-06-20 |
quigley |
Added VampCommunication.ML.
|
file |
diff |
annotate
|
2005-06-10 |
quigley |
All subgoals sent to the watcher at once now.
|
file |
diff |
annotate
|
2005-06-05 |
wenzelm |
File.platform_path;
|
file |
diff |
annotate
|
2005-05-31 |
paulson |
minor tidying and sml/nj compatibility
|
file |
diff |
annotate
|
2005-05-31 |
quigley |
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
|
file |
diff |
annotate
|
2005-05-26 |
paulson |
further tweaks to the SPASS setup
|
file |
diff |
annotate
|
2005-05-24 |
paulson |
A new structure and reduced indentation
|
file |
diff |
annotate
|
2005-05-22 |
quigley |
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
|
file |
diff |
annotate
|
2005-05-03 |
quigley |
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
|
file |
diff |
annotate
|
2005-04-22 |
paulson |
removed last occurrences of OS.Process.sleep
|
file |
diff |
annotate
|
2005-04-21 |
paulson |
added hearder lines and deleted some redundant material
|
file |
diff |
annotate
|
2005-04-21 |
paulson |
improved SML/NJ compatibility, etc.
|
file |
diff |
annotate
|
2005-04-20 |
quigley |
Corrected the problem with the ATP directory.
|
file |
diff |
annotate
|
2005-04-19 |
paulson |
more tidying of libraries in Reconstruction
|
file |
diff |
annotate
|
2005-04-15 |
paulson |
yet more tidying up: removal of some references to Main
|
file |
diff |
annotate
|
2005-04-12 |
paulson |
tweaks mainly to achieve sml/nj compatibility
|
file |
diff |
annotate
|
2005-04-11 |
paulson |
removal of Main and other tidying up
|
file |
diff |
annotate
|
2005-04-08 |
paulson |
Reconstruction code, now packaged to avoid name clashes
|
file |
diff |
annotate
|
2005-04-06 |
quigley |
watcher.ML and watcher.sig changed. Debug files now write to tmp.
|
file |
diff |
annotate
|
2005-03-31 |
quigley |
*** empty log message ***
|
file |
diff |
annotate
|