| Tue, 08 Aug 2006 18:40:56 +0200 |
paulson |
skolem declarations for built-in theorems
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:46 +0200 |
wenzelm |
removed obsolete Drule.freeze_all -- now uses legacy Drule.freeze_thaw;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:16:54 +0200 |
wenzelm |
replaced Term.variant(list) by Name.variant(_list);
|
file |
diff |
annotate
|
| Wed, 05 Jul 2006 16:24:10 +0200 |
paulson |
made the conversion of elimination rules more robust
|
file |
diff |
annotate
|
| Thu, 15 Jun 2006 17:50:47 +0200 |
paulson |
the "all_theorems" option and some fixes
|
file |
diff |
annotate
|
| Sat, 13 May 2006 02:51:42 +0200 |
wenzelm |
Theory.add_defs(_i): added unchecked flag;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2006 05:36:38 +0200 |
mengj |
Tidied up some programs.
|
file |
diff |
annotate
|
| Fri, 07 Apr 2006 05:12:23 +0200 |
mengj |
added another function for CNF.
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 12:28:38 +0100 |
paulson |
Changed some warnings to debug messages
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 16:47:51 +0100 |
paulson |
Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 03:56:59 +0100 |
mengj |
Added functions to retrieve local and global atpset rules.
|
file |
diff |
annotate
|
| Thu, 02 Mar 2006 18:50:43 +0100 |
paulson |
subset_refl now included using the atp attribute
|
file |
diff |
annotate
|
| Mon, 20 Feb 2006 16:23:38 +0100 |
paulson |
Inclusion of subset_refl in ATP calls
|
file |
diff |
annotate
|
| Fri, 03 Feb 2006 17:08:03 +0100 |
paulson |
removal of case analysis clauses
|
file |
diff |
annotate
|
| Sun, 29 Jan 2006 19:23:40 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:13 +0100 |
wenzelm |
Output.debug;
|
file |
diff |
annotate
|
| Tue, 10 Jan 2006 19:33:27 +0100 |
wenzelm |
Attrib.rule;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:40 +0100 |
wenzelm |
elim rules: Classical.classical_rule;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 17:37:54 +0100 |
paulson |
the "skolem" attribute and better initialization of the clause database
|
file |
diff |
annotate
|
| Wed, 14 Dec 2005 16:13:09 +0100 |
paulson |
removed unused function repeat_RS
|
file |
diff |
annotate
|
| Mon, 28 Nov 2005 07:15:38 +0100 |
mengj |
Added two functions for CNF translation, used by other files.
|
file |
diff |
annotate
|
| Fri, 18 Nov 2005 07:08:18 +0100 |
mengj |
-- combined common CNF functions used by HOL and FOL axioms, the difference between conversion of HOL and FOL theorems only comes in when theorems are converted to ResClause.clause or ResHolClause.clause format.
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 17:33:14 +0100 |
paulson |
duplicate axioms in ATP linkup, and general fixes
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 18:01:33 +0100 |
paulson |
Skolemization by inference, but not quite finished
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 12:22:34 +0200 |
paulson |
got rid of obsolete prove_goalw_cterm
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 02:25:57 +0200 |
mengj |
Added several new functions that convert HOL Isabelle rules to FOL axiom clauses. The original functions that convert FOL rules to clauses stay with the same names; the new functions have "H" at the end of their names.
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:38 +0200 |
wenzelm |
OldGoals;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 06:33:24 +0200 |
mengj |
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
|
file |
diff |
annotate
|
| Tue, 11 Oct 2005 15:04:11 +0200 |
paulson |
simplifying the treatment of clausification
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 15:35:29 +0200 |
paulson |
small tidy-up of utility functions
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 15:12:13 +0200 |
paulson |
simplification of the Isabelle-ATP code; hooks for batch generation of problems
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 11:15:52 +0200 |
paulson |
the experimental tagging system, and the usual tidying
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 16:59:54 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 17:38:18 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Wed, 27 Jul 2005 11:30:34 +0200 |
paulson |
simpler variable names, and no types for monomorphic constants
|
file |
diff |
annotate
|
| Wed, 20 Jul 2005 17:00:28 +0200 |
paulson |
code streamlining
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 16:07:21 +0200 |
wenzelm |
improved Net interface;
|
file |
diff |
annotate
|
| Tue, 28 Jun 2005 15:28:04 +0200 |
paulson |
stricter first-order check for meson
|
file |
diff |
annotate
|
| Fri, 24 Jun 2005 17:25:10 +0200 |
paulson |
meson method taking an argument list
|
file |
diff |
annotate
|
| Wed, 01 Jun 2005 18:19:59 +0200 |
paulson |
clausification bug fix
|
file |
diff |
annotate
|
| Tue, 31 May 2005 12:42:36 +0200 |
quigley |
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:16 +0200 |
wenzelm |
proper use of Sign.full_name;
|
file |
diff |
annotate
|
| Mon, 23 May 2005 00:18:51 +0200 |
quigley |
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
|
file |
diff |
annotate
|
| Fri, 20 May 2005 18:35:10 +0200 |
paulson |
bug fixes for clause form transformation
|
file |
diff |
annotate
|
| Thu, 19 May 2005 11:08:15 +0200 |
paulson |
Skolemization of simprules and classical rules
|
file |
diff |
annotate
|
| Wed, 18 May 2005 10:23:47 +0200 |
paulson |
consolidation and simplification
|
file |
diff |
annotate
|
| Thu, 12 May 2005 18:24:42 +0200 |
paulson |
theorem names for caching
|
file |
diff |
annotate
|
| Thu, 12 May 2005 15:42:58 +0200 |
paulson |
memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:56:58 +0200 |
paulson |
fixed treatment of higher-order simprules
|
file |
diff |
annotate
|
| Fri, 15 Apr 2005 13:35:53 +0200 |
paulson |
more tidying up of the SPASS interface
|
file |
diff |
annotate
|
| Fri, 08 Apr 2005 18:43:39 +0200 |
paulson |
Reconstruction code, now packaged to avoid name clashes
|
file |
diff |
annotate
|
| Thu, 31 Mar 2005 20:12:54 +0200 |
quigley |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 14 Mar 2005 17:04:10 +0100 |
paulson |
bug fixes involving typechecking clauses
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 16:55:36 +0100 |
paulson |
Tools/meson.ML: signature, structure and "open" rather than "local"
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Fri, 04 Feb 2005 18:35:46 +0100 |
paulson |
clausification and proof reconstruction
|
file |
diff |
annotate
|
| Thu, 03 Feb 2005 16:06:19 +0100 |
paulson |
new treatment of demodulation in proof reconstruction
|
file |
diff |
annotate
|