| Mon, 09 Oct 2006 02:19:54 +0200 |
wenzelm |
replaced Drule.clhs/crhs_of by Drule.lhs/rhs_of;
|
file |
diff |
annotate
|
| Fri, 06 Oct 2006 11:16:40 +0200 |
paulson |
Refinements to abstraction. Seeding with combinators K, I and B.
|
file |
diff |
annotate
|
| Thu, 05 Oct 2006 10:42:39 +0200 |
paulson |
improvements to abstraction, ensuring more re-use of abstraction functions
|
file |
diff |
annotate
|
| Sat, 30 Sep 2006 14:31:02 +0200 |
mengj |
Removed ResHolClause.LAM2COMB exception.
|
file |
diff |
annotate
|
| Fri, 29 Sep 2006 22:46:59 +0200 |
wenzelm |
Sign.add_consts_authentic;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:50 +0200 |
wenzelm |
ResAtpset.get_atpset;
|
file |
diff |
annotate
|
| Tue, 26 Sep 2006 11:09:33 +0200 |
paulson |
Abstraction now handles equations where the RHS is a lambda-expression; also, strings of lambdas
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 23:15:32 +0200 |
wenzelm |
sko/abs: Name.internal prevents choking of print_theory;
|
file |
diff |
annotate
|
| Mon, 18 Sep 2006 16:21:24 +0200 |
paulson |
Bug fix to prevent exception dest_Free from escaping
|
file |
diff |
annotate
|
| Wed, 13 Sep 2006 12:18:36 +0200 |
paulson |
bug fix to abstractions: free variables in theorem can be abstracted over.
|
file |
diff |
annotate
|
| Mon, 04 Sep 2006 18:41:33 +0200 |
paulson |
Using Drule.local_standard to reduce the space usage
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 23:04:42 +0200 |
wenzelm |
skolem_cache_thm: Drule.close_derivation on clauses preserves some space;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2006 08:51:53 +0200 |
paulson |
refinements to conversion into clause form, esp for the HO case
|
file |
diff |
annotate
|
| Thu, 31 Aug 2006 10:20:22 +0200 |
paulson |
improvements to abstraction generation
|
file |
diff |
annotate
|
| Mon, 28 Aug 2006 18:15:32 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Fri, 25 Aug 2006 18:48:58 +0200 |
paulson |
abstraction of lambda-expressions
|
file |
diff |
annotate
|
| Wed, 09 Aug 2006 18:41:42 +0200 |
paulson |
consistent prefixing for skolem functions
|
file |
diff |
annotate
|
| 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
|