src/Provers/splitter.ML
Sat, 25 Jul 2015 23:41:53 +0200 wenzelm updated to infer_instantiate;
Tue, 02 Jun 2015 11:03:02 +0200 wenzelm clarified context;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Sun, 09 Nov 2014 14:08:00 +0100 wenzelm proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
Thu, 30 Oct 2014 16:55:29 +0100 wenzelm eliminated aliases;
Wed, 29 Oct 2014 19:01:49 +0100 wenzelm modernized setup;
Thu, 11 Sep 2014 21:11:03 +0200 blanchet fixed some spelling mistakes
Wed, 27 Aug 2014 14:54:32 +0200 wenzelm more explicit Method.modifier with reported position;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Tue, 29 Oct 2013 13:48:18 +0100 berghofe inst_lift now fully instantiates context to avoid problems with loose bound variables
Fri, 24 May 2013 17:00:46 +0200 wenzelm tuned signature;
Thu, 16 May 2013 17:39:38 +0200 wenzelm tuned signature -- depend on context by default;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sat, 16 Apr 2011 20:30:44 +0200 wenzelm more direct Thm.cprem_of (with exception THM instead of Subscript);
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sun, 07 Mar 2010 12:19:47 +0100 wenzelm modernized structure Object_Logic;
Tue, 24 Nov 2009 17:28:25 +0100 haftmann curried take/drop
Thu, 29 Oct 2009 17:58:26 +0100 wenzelm standardized filter/filter_out;
Tue, 27 Oct 2009 22:56:14 +0100 wenzelm eliminated some old folds;
Tue, 27 Oct 2009 17:19:31 +0100 wenzelm misc tuning and simplification;
Tue, 20 Oct 2009 20:54:31 +0200 wenzelm uniform use of Integer.min/max;
Fri, 24 Jul 2009 21:34:37 +0200 wenzelm renamed functor SplitterFun to Splitter, require explicit theory;
Fri, 24 Jul 2009 21:02:34 +0200 wenzelm explicit OldGoals;
Thu, 26 Mar 2009 14:14:02 +0100 wenzelm simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
Fri, 20 Mar 2009 17:12:37 +0100 wenzelm Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
Wed, 18 Mar 2009 15:23:52 +0100 haftmann made SML/NJ happy
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute setup;
Fri, 13 Mar 2009 23:50:05 +0100 wenzelm simplified method setup;
Fri, 13 Mar 2009 21:25:15 +0100 wenzelm eliminated type Args.T;
Fri, 13 Mar 2009 19:58:26 +0100 wenzelm unified type Proof.method and pervasive METHOD combinators;
Sun, 18 Jan 2009 13:53:15 +0100 nipkow bug fixes
Tue, 18 Nov 2008 18:25:42 +0100 wenzelm eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
Thu, 17 Apr 2008 22:22:21 +0200 wenzelm prove_global: pass context;
Tue, 25 Sep 2007 13:28:37 +0200 wenzelm Syntax.parse/check/read;
Sun, 06 May 2007 21:49:23 +0200 haftmann tuned
Sat, 14 Apr 2007 17:35:52 +0200 wenzelm cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
Wed, 04 Apr 2007 23:29:33 +0200 wenzelm rep_thm/cterm/ctyp: removed obsolete sign field;
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Mon, 18 Dec 2006 08:21:35 +0100 haftmann switched argument order in *.syntax lifters
Wed, 29 Nov 2006 15:44:51 +0100 wenzelm simplified method setup;
Thu, 21 Sep 2006 19:04:20 +0200 wenzelm member (op =);
Thu, 27 Jul 2006 14:21:57 +0200 webertj type annotation added to make SML/NJ happy
Wed, 26 Jul 2006 19:23:04 +0200 webertj linear arithmetic splits certain operators (e.g. min, max, abs)
Fri, 10 Feb 2006 02:22:16 +0100 wenzelm Args/Attrib syntax: Context.generic;
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 22:25:34 +0100 wenzelm generic attributes;
Tue, 03 Jan 2006 00:06:26 +0100 wenzelm avoid hardwired Trueprop;
Thu, 10 Nov 2005 20:57:11 +0100 wenzelm renamed Thm.cgoal_of to Thm.cprem_of;
Fri, 28 Oct 2005 22:27:47 +0200 wenzelm accomodate simplified Thm.lift_rule;
Fri, 21 Oct 2005 18:14:38 +0200 wenzelm OldGoals;
Mon, 17 Oct 2005 23:10:19 +0200 wenzelm functor: no Simplifier argument;
Mon, 12 Sep 2005 18:20:32 +0200 haftmann introduced new-style AList operations
Mon, 29 Aug 2005 16:18:04 +0200 wenzelm use AList operations;
less more (0) -100 -60 tip