src/Provers/classical.ML
Wed, 27 Aug 2014 14:54:32 +0200 wenzelm more explicit Method.modifier with reported position;
Tue, 05 Aug 2014 12:01:32 +0200 wenzelm more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
Mon, 31 Mar 2014 12:35:39 +0200 wenzelm some shortcuts for chunks, which sometimes avoid bulky string output;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Sat, 27 Jul 2013 16:35:51 +0200 wenzelm standardized aliases;
Thu, 18 Jul 2013 21:20:09 +0200 wenzelm tuned signature;
Thu, 27 Jun 2013 10:14:17 +0200 wenzelm actually use Data.sizef, not hardwired size_of_thm;
Sat, 27 Apr 2013 20:50:20 +0200 wenzelm uniform Proof.context for hyp_subst_tac;
Thu, 18 Apr 2013 21:10:12 +0200 wenzelm tuned signature;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Fri, 12 Apr 2013 17:21:51 +0200 wenzelm modifiers for classical wrappers operate on Proof.context instead of claset;
Wed, 10 Apr 2013 17:27:38 +0200 wenzelm obsolete -- tools should refer to proper Proof.context;
Tue, 09 Apr 2013 15:29:25 +0200 wenzelm discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
Sat, 30 Mar 2013 13:40:19 +0100 wenzelm more item markup;
Fri, 29 Mar 2013 22:14:27 +0100 wenzelm Pretty.item markup for improved readability of lists of items;
Sat, 17 Nov 2012 20:38:57 +0100 wenzelm tuned -- eliminate pointless ML method definition;
Sat, 17 Nov 2012 19:46:32 +0100 wenzelm method setup for Classical steps;
Sat, 03 Nov 2012 19:07:07 +0100 wenzelm more concise/precise documentation;
Mon, 25 Jun 2012 17:44:16 +0200 wenzelm prefer direct rotate_prems over old-style COMP;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Mon, 12 Mar 2012 15:31:30 +0100 wenzelm tuned signature;
Tue, 14 Feb 2012 17:11:33 +0100 wenzelm eliminated obsolete aliases;
Sun, 06 Nov 2011 21:51:46 +0100 wenzelm more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
Sun, 15 May 2011 19:19:26 +0200 wenzelm tuned;
Sun, 15 May 2011 16:40:24 +0200 wenzelm tuned signature;
Sat, 14 May 2011 21:42:17 +0200 wenzelm slightly more efficient claset operations, using Item_Net to maintain rules in canonical order;
Sat, 14 May 2011 17:55:08 +0200 wenzelm more precise warnings: observe context visibility;
Sat, 14 May 2011 11:42:43 +0200 wenzelm modernized functor names;
Sat, 14 May 2011 00:32:16 +0200 wenzelm method "deepen" with optional limit;
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
less more (0) -100 -50 -30 tip