src/Provers/clasimp.ML
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;
1999-08-18 wenzelm 1999-08-18 Method.modifier;
1999-08-02 wenzelm 1999-08-02 tuned;
1999-07-30 wenzelm 1999-07-30 eliminated METHOD0 in favour of same_tac;
1998-11-29 wenzelm 1998-11-29 method brute_force = ALLGOALS force_tac;
1998-11-18 wenzelm 1998-11-18 method setup;
1998-10-23 oheimb 1998-10-23 corrected auto_tac (applications of unsafe wrappers) by correcting (and simplifying) nodup_depth_tac
1998-09-25 paulson 1998-09-25 deleted illegal "op"
1998-09-24 oheimb 1998-09-24 removed addcongs2 and delcongs2 simplified CLASIMP_DATA
1998-09-21 oheimb 1998-09-21 improved addbefore and addSbefore improved mechanism for unsafe wrappers
1998-09-11 oheimb 1998-09-11 added clarsimp_tac and Clarsimp_tac
1998-07-30 wenzelm 1998-07-30 functorized Clasimp module;
1998-05-02 wenzelm 1998-05-02 added CLASIMPSET(') tacticals;
1998-05-01 oheimb 1998-05-01 Auto_tac: now uses enhanced version of asm_full_simp_tac, Force_tac: replaced fast_tac by best_tac
1998-03-10 oheimb 1998-03-10 renamed smart_tac to force_tac, slight improvement of force_tac
1998-02-26 oheimb 1998-02-26 added smart_tac
1998-02-25 oheimb 1998-02-25 factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset