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