| 2007-05-08 |
wenzelm |
2007-05-08 |
tuned;
|
file | diff | annotate |
| 2007-04-18 |
paulson |
2007-04-18 |
Fixes for proof reconstruction, especially involving abstractions and definitions
|
file | diff | annotate |
| 2007-04-12 |
paulson |
2007-04-12 |
Zero variable indexes in clauses
|
file | diff | annotate |
| 2007-03-29 |
paulson |
2007-03-29 |
MESON tactical takes an additional argument: the clausification function.
|
file | diff | annotate |
| 2007-03-26 |
paulson |
2007-03-26 |
"generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
Improved comments and tidying.
|
file | diff | annotate |
| 2007-03-02 |
paulson |
2007-03-02 |
The first-order test now tests for the obscure case of a polymorphic constant like 1 being
used with a function type.
|
file | diff | annotate |
| 2007-02-26 |
wenzelm |
2007-02-26 |
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
|
file | diff | annotate |
| 2007-01-20 |
wenzelm |
2007-01-20 |
Output.debug: non-strict;
renamed Output.show_debug_msgs to Output.debugging (coincides with Toplevel.debug);
|
file | diff | annotate |
| 2007-01-04 |
paulson |
2007-01-04 |
improvements to proof reconstruction. Some files loaded in a different order
|
file | diff | annotate |
| 2006-12-22 |
paulson |
2006-12-22 |
tidying the ATP communications
|
file | diff | annotate |
| 2006-12-06 |
wenzelm |
2006-12-06 |
LocalDefs.expand;
|
file | diff | annotate |
| 2006-12-05 |
wenzelm |
2006-12-05 |
thm/prf: separate official name vs. additional tags;
|
file | diff | annotate |
| 2006-12-01 |
paulson |
2006-12-01 |
Fixed a MAJOR BUG in clause-counting: only Boolean equalities now count as iffs
|
file | diff | annotate |
| 2006-11-29 |
wenzelm |
2006-11-29 |
simplified method setup;
|
file | diff | annotate |
| 2006-11-04 |
wenzelm |
2006-11-04 |
removed is_Trueprop (use can dest_Trueprop'' instead);
|
file | diff | annotate |
| 2006-10-26 |
paulson |
2006-10-26 |
Conversion to clause form now tolerates Boolean variables without looping.
Attribute "clausify" moved to res_axioms; rest of reconstruction.ML deleted
|
file | diff | annotate |
| 2006-10-23 |
paulson |
2006-10-23 |
Improved tracing
|
file | diff | annotate |
| 2006-10-20 |
paulson |
2006-10-20 |
nclauses no longer requires its input to be in NNF
|
file | diff | annotate |
| 2006-10-18 |
paulson |
2006-10-18 |
More robust error handling in make_nnf and forward_res
|
file | diff | annotate |
| 2006-10-16 |
haftmann |
2006-10-16 |
moved HOL code generator setup to Code_Generator
|
file | diff | annotate |
| 2006-10-11 |
haftmann |
2006-10-11 |
abandoned findrep
|
file | diff | annotate |
| 2006-10-02 |
paulson |
2006-10-02 |
Now checks explicitly for Trueprop, thereby ignoring junk theorems involving OF_CLASS, etc.
|
file | diff | annotate |
| 2006-09-13 |
paulson |
2006-09-13 |
Tweaks to is_fol_term, the first-order test. We don't count "=" as a connective
since this test is applied to clause forms.
|
file | diff | annotate |
| 2006-08-25 |
paulson |
2006-08-25 |
better skolemization, using first-order resolution rather than hoping for the right result
|
file | diff | annotate |
| 2006-08-08 |
paulson |
2006-08-08 |
more explict variable names
|
file | diff | annotate |
| 2006-08-02 |
wenzelm |
2006-08-02 |
simplified Assumption/ProofContext.export;
|
file | diff | annotate |
| 2006-07-16 |
paulson |
2006-07-16 |
has_consts renamed to has_conn, now actually parses the first-order formula
to avoid problems caused by connectives buried within descriptions and set comprehensions.
|
file | diff | annotate |
| 2006-07-13 |
paulson |
2006-07-13 |
fix to refl_clause_aux: added occurs check
|
file | diff | annotate |
| 2006-07-11 |
wenzelm |
2006-07-11 |
removed obsolete mem_term;
|
file | diff | annotate |
| 2006-07-05 |
paulson |
2006-07-05 |
removed the "tagging" feature
|
file | diff | annotate |
| 2006-06-15 |
paulson |
2006-06-15 |
the "all_theorems" option and some fixes
|
file | diff | annotate |
| 2006-06-13 |
wenzelm |
2006-06-13 |
avoid unqualified exception names;
tuned;
|
file | diff | annotate |
| 2006-05-26 |
wenzelm |
2006-05-26 |
freeze_spec: gensym;
|
file | diff | annotate |
| 2006-03-07 |
paulson |
2006-03-07 |
Tidying, and getting rid of SELECT_GOAL (as it does something different now)
|
file | diff | annotate |
| 2006-02-28 |
paulson |
2006-02-28 |
fixed but in freeze_spec
|
file | diff | annotate |
| 2006-02-20 |
paulson |
2006-02-20 |
Fix variable-naming bug (?) by removing a needless recursive call
|
file | diff | annotate |
| 2006-02-15 |
wenzelm |
2006-02-15 |
removed distinct, renamed gen_distinct to distinct;
|
file | diff | annotate |
| 2006-01-28 |
wenzelm |
2006-01-28 |
LocalDefs.def_export;
|
file | diff | annotate |
| 2006-01-23 |
paulson |
2006-01-23 |
Clausification now handles some IFs in rewrite rules (if-split did not work)
|
file | diff | annotate |
| 2006-01-19 |
wenzelm |
2006-01-19 |
setup: theory -> theory;
|
file | diff | annotate |
| 2006-01-14 |
wenzelm |
2006-01-14 |
Output.debug;
|
file | diff | annotate |
| 2006-01-13 |
wenzelm |
2006-01-13 |
ProofContext.def_export;
|
file | diff | annotate |
| 2005-12-23 |
paulson |
2005-12-23 |
tidied
|
file | diff | annotate |
| 2005-12-14 |
paulson |
2005-12-14 |
removal of some redundancies (e.g. one-point-rules) in clause production
|
file | diff | annotate |
| 2005-12-13 |
paulson |
2005-12-13 |
removal of functional reflexivity axioms
|
file | diff | annotate |
| 2005-11-18 |
mengj |
2005-11-18 |
-- removed "check_is_fol" from "make_nnf" so that the NNF procedure doesn't check whether a thm is FOL.
-- added "check_is_fol_term", which is the same as "check_is_fol", but takes a "term" as input.
-- added "check_is_fol" and "check_is_fol_term" into the signature.
|
file | diff | annotate |
| 2005-11-16 |
paulson |
2005-11-16 |
new version of "tryres" allowing multiple unifiers (apparently needed for
Skolemization of higher-order theorems)
|
file | diff | annotate |
| 2005-11-09 |
paulson |
2005-11-09 |
Skolemization by inference, but not quite finished
|
file | diff | annotate |
| 2005-10-28 |
wenzelm |
2005-10-28 |
renamed Goal constant to prop;
|
file | diff | annotate |
| 2005-10-14 |
paulson |
2005-10-14 |
signature changes
|
file | diff | annotate |
| 2005-09-29 |
paulson |
2005-09-29 |
moved concat_with_and to watcher.ML
|
file | diff | annotate |
| 2005-09-15 |
paulson |
2005-09-15 |
the experimental tagging system, and the usual tidying
|
file | diff | annotate |
| 2005-07-13 |
wenzelm |
2005-07-13 |
tuned concat_with_and;
improved Net interface;
|
file | diff | annotate |
| 2005-06-28 |
paulson |
2005-06-28 |
stricter first-order check for meson
|
file | diff | annotate |
| 2005-06-24 |
paulson |
2005-06-24 |
meson method taking an argument list
|
file | diff | annotate |
| 2005-06-01 |
paulson |
2005-06-01 |
clausification bug fix
|
file | diff | annotate |
| 2005-05-20 |
paulson |
2005-05-20 |
bug fixes for clause form transformation
|
file | diff | annotate |
| 2005-05-18 |
paulson |
2005-05-18 |
new cnf function taking Skolemization theorems as an extra argument
|
file | diff | annotate |
| 2005-05-16 |
paulson |
2005-05-16 |
Use of IntInf.int instead of int in most numeric simprocs; avoids
integer overflow in SML/NJ
|
file | diff | annotate |
| 2005-05-09 |
paulson |
2005-05-09 |
unfolding of Ex1
|
file | diff | annotate |