src/Provers/clasimp.ML
6 months ago wenzelm 2019-01-04 isabelle update -u control_cartouches;
2016-12-13 wenzelm 2016-12-13 more symbols;
2015-08-16 wenzelm 2015-08-16 tuned signature;
2015-06-02 wenzelm 2015-06-02 tuned;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2014-08-19 wenzelm 2014-08-19 added PARALLEL_ALLGOALS convenience;
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-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-12 wenzelm 2013-04-12 modifiers for classical wrappers operate on Proof.context instead of claset;
2012-11-17 wenzelm 2012-11-17 tuned;
2012-11-17 wenzelm 2012-11-17 tuned signature;
2012-05-23 wenzelm 2012-05-23 discontinued obsolete method fastsimp / tactic fast_simp_tac;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-06-09 wenzelm 2011-06-09 clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b); uniform handling of exceptions in depth_tac and blast_tac, discontinued separate blast_depth_tac; tuned blast_tac: atomize prems only once, outside DEEPEN;
2011-05-14 wenzelm 2011-05-14 discontinued old / unused addss' (cf. 57f364d1d3b2);
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-05-13 wenzelm 2011-05-13 simplified clasimpset declarations -- prefer attributes;
2011-04-26 wenzelm 2011-04-26 tuned;
2011-04-26 wenzelm 2011-04-26 modernized Clasimp setup;
2011-04-16 wenzelm 2011-04-16 PARALLEL_GOALS for simplification within auto_tac;
2010-07-05 paulson 2010-07-05 Unification (flexflex) bug fix; making "auto" deterministic
2010-05-17 wenzelm 2010-05-17 prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
2010-04-30 wenzelm 2010-04-30 map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2009-11-01 wenzelm 2009-11-01 modernized structure Context_Rules;
2009-10-02 wenzelm 2009-10-02 eliminated dead code;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
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-15 wenzelm 2009-03-15 simplified method setup;
2009-03-15 wenzelm 2009-03-15 simplified attribute 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-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2008-08-09 wenzelm 2008-08-09 unified Args.T with OuterLex.token, renamed some operations;
2008-03-29 wenzelm 2008-03-29 purely functional setup of claset/simpset/clasimpset; tuned signature;
2008-03-27 wenzelm 2008-03-27 renamed ML_Context.the_context to ML_Context.the_global_context;
2007-01-19 wenzelm 2007-01-19 moved ML context stuff to from Context to ML_Context;
2006-12-30 wenzelm 2006-12-30 removed obsolete name_hint handling;
2006-12-08 paulson 2006-12-08 removed use of put_name_hint, as the ATP linkup no longer needs this
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
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-10 wenzelm 2006-01-10 generic attributes; added low-level modifiers from Pure/context_rules.ML;
2005-12-31 wenzelm 2005-12-31 removed obsolete Provers/make_elim.ML;
2005-12-21 paulson 2005-12-21 modified suffix for [iff] attribute
2005-10-17 wenzelm 2005-10-17 functor: no Simplifier argument; export change_clasimpset;
2005-08-16 paulson 2005-08-16 classical rules must have names for ATP integration
2005-05-22 wenzelm 2005-05-22 Simplifier already setup in Pure;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-07-11 wenzelm 2004-07-11 local_cla/simpset_of;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-09-30 berghofe 2002-09-30 Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
2002-03-05 wenzelm 2002-03-05 iff: conditional rules declared as ``unsafe'';
2001-12-05 wenzelm 2001-12-05 iff?: refer to Pure/ContextRules;
2001-10-23 wenzelm 2001-10-23 iff: always rotate prems;