src/Provers/splitter.ML
2015-07-25 wenzelm 2015-07-25 updated to infer_instantiate; tuned;
2015-06-02 wenzelm 2015-06-02 clarified context;
2015-04-08 wenzelm 2015-04-08 proper context for Object_Logic operations;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-11 blanchet 2014-09-11 fixed some spelling mistakes
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-10-29 berghofe 2013-10-29 inst_lift now fully instantiates context to avoid problems with loose bound variables
2013-05-24 wenzelm 2013-05-24 tuned signature;
2013-05-16 wenzelm 2013-05-16 tuned signature -- depend on context by default;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-04-16 wenzelm 2011-04-16 more direct Thm.cprem_of (with exception THM instead of Subscript); modernized thy;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-27 wenzelm 2009-10-27 misc tuning and simplification;
2009-10-20 wenzelm 2009-10-20 uniform use of Integer.min/max;
2009-07-24 wenzelm 2009-07-24 renamed functor SplitterFun to Splitter, require explicit theory;
2009-07-24 wenzelm 2009-07-24 explicit OldGoals;
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-18 haftmann 2009-03-18 made SML/NJ happy
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 simplified method setup;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-01-18 nipkow 2009-01-18 bug fixes
2008-11-18 wenzelm 2008-11-18 eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion; eliminated obsolete alias rewtac for rewrite_goals_tac;
2008-04-17 wenzelm 2008-04-17 prove_global: pass context;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-05-06 haftmann 2007-05-06 tuned
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 wenzelm 2007-04-04 removed obsolete sign_of/sign_of_thm;
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-07-27 webertj 2006-07-27 type annotation added to make SML/NJ happy
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-02-10 wenzelm 2006-02-10 Args/Attrib syntax: Context.generic;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 generic attributes;
2006-01-03 wenzelm 2006-01-03 avoid hardwired Trueprop; local proof: static refererence to Pure.thy;
2005-11-10 wenzelm 2005-11-10 renamed Thm.cgoal_of to Thm.cprem_of;
2005-10-28 wenzelm 2005-10-28 accomodate simplified Thm.lift_rule;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-17 wenzelm 2005-10-17 functor: no Simplifier argument; change_simpset;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-08-29 wenzelm 2005-08-29 use AList operations;