src/Provers/clasimp.ML
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;
2001-08-09 oheimb 2001-08-09 corrected semantics of [iff] concerning rules with premises
2001-08-06 paulson 2001-08-06 removed the warning from [iff]
2001-05-31 oheimb 2001-05-31 streamlined addIffs/delIffs, added warnings
2001-02-23 oheimb 2001-02-23 renamed addaltern to addafter, addSaltern to addSafter
2001-01-07 wenzelm 2001-01-07 CHANGED_PROP;
2000-10-24 wenzelm 2000-10-24 added clasimpset: unit -> clasimpset;
2000-09-20 wenzelm 2000-09-20 made SML/NJ happy;
2000-09-19 wenzelm 2000-09-19 added iff_add_global', iff_add_local' (syntax "iff?"); tuned;
2000-09-13 wenzelm 2000-09-13 Args.addN, Args.delN;
2000-09-07 wenzelm 2000-09-07 tuned msg;
2000-09-05 wenzelm 2000-09-05 added 'iff' declarations;
2000-09-02 wenzelm 2000-09-02 added "slowsimp", "bestsimp";
2000-09-01 wenzelm 2000-09-01 auto method: opt args; tuned;
2000-08-14 wenzelm 2000-08-14 added "fastsimp"; fixed "clarsimp": CHANGED;
2000-08-03 wenzelm 2000-08-03 export get_local_clasimpset, clasimp_modifiers;
2000-07-25 wenzelm 2000-07-25 added clarsimp method;
2000-07-21 oheimb 2000-07-21 strengthened force_tac by using new first_best_tac
2000-03-31 wenzelm 2000-03-31 added change_global/local_css;
2000-03-15 wenzelm 2000-03-15 include Splitter.split_modifiers;
2000-01-28 wenzelm 2000-01-28 HEADGOAL;
2000-01-28 wenzelm 2000-01-28 replaced FIRSTGOAL by FINDGOAL (backtracking!);
1999-10-27 oheimb 1999-10-27 clarsimp_tac now copes with the (unwanted) case that the simplifier splits the goal
1999-09-21 wenzelm 1999-09-21 setup for refined facts handling; Method.bang_sectioned_args / Args.bang_facts;
1999-09-02 wenzelm 1999-09-02 renamed improper method 'clarsimp' to 'clarsimp_tac';
1999-09-01 wenzelm 1999-09-01 Method.insert_tac;
1999-08-30 wenzelm 1999-08-30 auto: CHANGED;