src/Provers/classical.ML
Sat, 31 Dec 2005 21:49:42 +0100 wenzelm added classical_rule, which replaces Data.make_elim;
Thu, 08 Dec 2005 20:16:04 +0100 wenzelm swap: no longer pervasive;
Tue, 22 Nov 2005 19:34:41 +0100 wenzelm Drule.multi_resolves;
Fri, 28 Oct 2005 17:59:07 +0200 berghofe Added "deepen" method.
Mon, 17 Oct 2005 23:10:18 +0200 wenzelm change_claset(_of): more abtract interface;
Sat, 08 Oct 2005 20:15:34 +0200 wenzelm minor tweaks for Poplog/PML;
Mon, 05 Sep 2005 08:14:35 +0200 haftmann introduced binding priority 1 for linear combinators etc.
Tue, 16 Aug 2005 15:36:28 +0200 paulson classical rules must have names for ATP integration
Tue, 16 Aug 2005 13:42:26 +0200 wenzelm OuterKeyword;
Wed, 13 Jul 2005 16:07:27 +0200 wenzelm removed obsolete delta stuff;
Fri, 17 Jun 2005 18:33:05 +0200 wenzelm accomodate change of TheoryDataFun;
Fri, 15 Apr 2005 12:00:00 +0200 ballarin Removed most of the atp interface from Pure.
Wed, 13 Apr 2005 18:45:52 +0200 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
Wed, 13 Apr 2005 18:34:22 +0200 wenzelm *** empty log message ***
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Fri, 21 Jan 2005 18:00:18 +0100 paulson Jia Meng: delta simpsets and clasets
Sun, 11 Jul 2004 20:35:50 +0200 wenzelm context dependent components;
Fri, 16 Apr 2004 20:59:09 +0200 wenzelm 'instance' and intro_classes now handle general sorts;
Tue, 27 Aug 2002 11:04:00 +0200 wenzelm dup_elim: improved error reporting;
Tue, 07 May 2002 14:26:32 +0200 wenzelm use eq_thm_prop instead of slightly inadequate eq_thm;
Thu, 06 Dec 2001 00:41:37 +0100 wenzelm added 'swapped' attribute;
Wed, 05 Dec 2001 03:12:52 +0100 wenzelm simplified (and clarified) integration with Pure/ContextRules;
Tue, 04 Dec 2001 18:10:49 +0100 wenzelm made SML/NJ happy;
Wed, 28 Nov 2001 00:46:26 +0100 wenzelm theory data: removed obsolete finish method;
Thu, 08 Nov 2001 23:59:37 +0100 wenzelm theory data: finish method;
Mon, 05 Nov 2001 20:56:29 +0100 wenzelm Method.trace ctxt;
Mon, 15 Oct 2001 20:36:04 +0200 wenzelm Tactic.orderlist;
Sun, 14 Oct 2001 20:04:05 +0200 wenzelm ObjectLogic.atomize_tac;
Fri, 12 Oct 2001 12:05:02 +0200 wenzelm moved trace_rules to Pure/Isar/method.ML;
Fri, 23 Feb 2001 16:31:21 +0100 oheimb renamed addaltern to addafter, addSaltern to addSafter
Tue, 20 Feb 2001 18:47:32 +0100 oheimb corrected comments on addbefore and addSbefore
Sun, 07 Jan 2001 21:41:56 +0100 wenzelm CHANGED_PROP;
Sat, 23 Dec 2000 22:52:18 +0100 wenzelm recover_order for single step tules;
Sat, 04 Nov 2000 18:44:34 +0100 wenzelm tuned method "rule" and "default";
Fri, 03 Nov 2000 21:29:56 +0100 wenzelm atomize: all automated tactics that "solve" goals;
Mon, 23 Oct 2000 22:10:36 +0200 wenzelm intro_classes by default;
Wed, 11 Oct 2000 00:03:22 +0200 wenzelm fixed 'clarify': CHANGED;
Tue, 19 Sep 2000 23:53:00 +0200 wenzelm tuned args;
Wed, 13 Sep 2000 22:31:19 +0200 wenzelm Args.addN, Args.delN;
Tue, 12 Sep 2000 22:13:23 +0200 wenzelm renamed atts: rulify to rule_format, elimify to elim_format;
Tue, 12 Sep 2000 17:38:49 +0200 wenzelm delrule: handle dest rules as well;
Thu, 07 Sep 2000 20:56:04 +0200 wenzelm tuned att names / msgs;
Sat, 02 Sep 2000 21:51:32 +0200 wenzelm added "slow";
Fri, 01 Sep 2000 00:31:39 +0200 wenzelm added "safe" method;
Thu, 31 Aug 2000 00:15:09 +0200 wenzelm improved messages;
Tue, 29 Aug 2000 15:13:10 +0200 nipkow *** empty log message ***
Wed, 09 Aug 2000 20:59:23 +0200 wenzelm fixed classification of rules in atts and modifiers (final!?);
Thu, 03 Aug 2000 18:44:24 +0200 wenzelm unknown_theory/proof/context;
Thu, 27 Jul 2000 11:44:29 +0200 wenzelm intro_elim_tac: bimatch_from;
Tue, 25 Jul 2000 00:13:49 +0200 wenzelm added clarify method;
Sun, 23 Jul 2000 12:01:05 +0200 wenzelm classical atts now intro! / intro / intro?;
Fri, 21 Jul 2000 17:46:43 +0200 oheimb strengthened force_tac by using new first_best_tac
Wed, 28 Jun 2000 21:15:02 +0200 wenzelm classical 'elimify' attribute;
Wed, 28 Jun 2000 10:55:38 +0200 paulson uses a supplied version of make_elim for addDs
Wed, 31 May 2000 14:29:42 +0200 wenzelm Toplevel.no_timing;
Tue, 23 May 2000 12:13:45 +0200 wenzelm improved warning messages;
Mon, 17 Apr 2000 14:10:04 +0200 wenzelm Pretty.chunks;
Thu, 13 Apr 2000 15:00:42 +0200 wenzelm intro/elim_tac: match only;
less more (0) -100 -60 tip