| 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
|