src/Provers/clasimp.ML
Wed, 27 Aug 2014 14:54:32 +0200 wenzelm more explicit Method.modifier with reported position;
Tue, 19 Aug 2014 17:00:44 +0200 wenzelm added PARALLEL_ALLGOALS convenience;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Fri, 12 Apr 2013 17:21:51 +0200 wenzelm modifiers for classical wrappers operate on Proof.context instead of claset;
Sat, 17 Nov 2012 20:29:17 +0100 wenzelm tuned;
Sat, 17 Nov 2012 17:55:52 +0100 wenzelm tuned signature;
Wed, 23 May 2012 16:22:27 +0200 wenzelm discontinued obsolete method fastsimp / tactic fast_simp_tac;
Sun, 06 Nov 2011 21:51:46 +0100 wenzelm more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
Mon, 12 Sep 2011 07:55:43 +0200 nipkow new fastforce replacing fastsimp - less confusing name
Thu, 09 Jun 2011 22:13:21 +0200 wenzelm clarified raw_blast, which is not really a tactic since it operates directly on subgoal 1 without bounds check (cf. c46107e6714b);
Sat, 14 May 2011 16:22:53 +0200 wenzelm discontinued old / unused addss' (cf. 57f364d1d3b2);
Fri, 13 May 2011 22:55:00 +0200 wenzelm proper Proof.context for classical tactics;
Fri, 13 May 2011 13:45:20 +0200 wenzelm simplified clasimpset declarations -- prefer attributes;
Tue, 26 Apr 2011 21:55:11 +0200 wenzelm tuned;
Tue, 26 Apr 2011 21:49:39 +0200 wenzelm modernized Clasimp setup;
Sat, 16 Apr 2011 23:41:58 +0200 wenzelm PARALLEL_GOALS for simplification within auto_tac;
Mon, 05 Jul 2010 14:21:30 +0100 paulson Unification (flexflex) bug fix; making "auto" deterministic
Mon, 17 May 2010 23:54:15 +0200 wenzelm prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
Fri, 30 Apr 2010 23:40:14 +0200 wenzelm map_css: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
Sat, 06 Mar 2010 15:39:16 +0100 wenzelm eliminated Args.bang_facts (legacy feature);
Sun, 01 Nov 2009 15:44:26 +0100 wenzelm modernized structure Context_Rules;
Fri, 02 Oct 2009 22:15:08 +0200 wenzelm eliminated dead code;
Thu, 23 Jul 2009 18:44:08 +0200 wenzelm renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
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;
Sun, 15 Mar 2009 20:25:58 +0100 wenzelm simplified method setup;
Sun, 15 Mar 2009 15:59:44 +0100 wenzelm simplified attribute 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, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Sat, 09 Aug 2008 22:43:46 +0200 wenzelm unified Args.T with OuterLex.token, renamed some operations;
Sat, 29 Mar 2008 22:55:57 +0100 wenzelm purely functional setup of claset/simpset/clasimpset;
Thu, 27 Mar 2008 14:41:10 +0100 wenzelm renamed ML_Context.the_context to ML_Context.the_global_context;
Fri, 19 Jan 2007 22:08:02 +0100 wenzelm moved ML context stuff to from Context to ML_Context;
Sat, 30 Dec 2006 16:08:03 +0100 wenzelm removed obsolete name_hint handling;
Fri, 08 Dec 2006 13:40:26 +0100 paulson removed use of put_name_hint, as the ATP linkup no longer needs this
Tue, 05 Dec 2006 00:30:38 +0100 wenzelm thm/prf: separate official name vs. additional tags;
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, 10 Jan 2006 19:33:29 +0100 wenzelm generic attributes;
Sat, 31 Dec 2005 21:49:36 +0100 wenzelm removed obsolete Provers/make_elim.ML;
Wed, 21 Dec 2005 12:05:47 +0100 paulson modified suffix for [iff] attribute
Mon, 17 Oct 2005 23:10:17 +0200 wenzelm functor: no Simplifier argument;
Tue, 16 Aug 2005 15:36:28 +0200 paulson classical rules must have names for ATP integration
Sun, 22 May 2005 16:51:07 +0200 wenzelm Simplifier already setup in Pure;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Sun, 11 Jul 2004 20:33:22 +0200 wenzelm local_cla/simpset_of;
Mon, 21 Jun 2004 10:25:57 +0200 kleing Merged in license change from Isabelle2004
Mon, 30 Sep 2002 16:32:05 +0200 berghofe Introduced addss', which adds asm_lr_simp_tac as a wrapper to the claset.
Tue, 05 Mar 2002 20:55:20 +0100 wenzelm iff: conditional rules declared as ``unsafe'';
Wed, 05 Dec 2001 03:11:05 +0100 wenzelm iff?: refer to Pure/ContextRules;
Tue, 23 Oct 2001 19:13:44 +0200 wenzelm iff: always rotate prems;
Thu, 09 Aug 2001 19:33:22 +0200 oheimb corrected semantics of [iff] concerning rules with premises
Mon, 06 Aug 2001 12:46:21 +0200 paulson removed the warning from [iff]
Thu, 31 May 2001 16:52:02 +0200 oheimb streamlined addIffs/delIffs, added warnings
Fri, 23 Feb 2001 16:31:21 +0100 oheimb renamed addaltern to addafter, addSaltern to addSafter
Sun, 07 Jan 2001 21:41:56 +0100 wenzelm CHANGED_PROP;
Tue, 24 Oct 2000 17:35:22 +0200 wenzelm added clasimpset: unit -> clasimpset;
Wed, 20 Sep 2000 00:02:26 +0200 wenzelm made SML/NJ happy;
Tue, 19 Sep 2000 23:52:37 +0200 wenzelm added iff_add_global', iff_add_local' (syntax "iff?");
Wed, 13 Sep 2000 22:31:19 +0200 wenzelm Args.addN, Args.delN;
Thu, 07 Sep 2000 20:51:07 +0200 wenzelm tuned msg;
Tue, 05 Sep 2000 18:50:12 +0200 wenzelm added 'iff' declarations;
Sat, 02 Sep 2000 21:51:14 +0200 wenzelm added "slowsimp", "bestsimp";
Fri, 01 Sep 2000 00:31:08 +0200 wenzelm auto method: opt args;
Mon, 14 Aug 2000 14:53:26 +0200 wenzelm added "fastsimp";
Thu, 03 Aug 2000 00:44:49 +0200 wenzelm export get_local_clasimpset, clasimp_modifiers;
Tue, 25 Jul 2000 00:13:11 +0200 wenzelm added clarsimp method;
Fri, 21 Jul 2000 17:46:43 +0200 oheimb strengthened force_tac by using new first_best_tac
Fri, 31 Mar 2000 21:58:34 +0200 wenzelm added change_global/local_css;
Wed, 15 Mar 2000 18:40:03 +0100 wenzelm include Splitter.split_modifiers;
Fri, 28 Jan 2000 21:57:15 +0100 wenzelm HEADGOAL;
Fri, 28 Jan 2000 12:12:06 +0100 wenzelm replaced FIRSTGOAL by FINDGOAL (backtracking!);
Wed, 27 Oct 1999 19:29:47 +0200 oheimb clarsimp_tac now copes with the (unwanted) case that the simplifier splits
Tue, 21 Sep 1999 17:26:50 +0200 wenzelm setup for refined facts handling;
Thu, 02 Sep 1999 15:21:36 +0200 wenzelm renamed improper method 'clarsimp' to 'clarsimp_tac';
Wed, 01 Sep 1999 21:22:56 +0200 wenzelm Method.insert_tac;
Mon, 30 Aug 1999 17:26:43 +0200 wenzelm auto: CHANGED;
Wed, 18 Aug 1999 20:47:31 +0200 wenzelm Method.modifier;
Mon, 02 Aug 1999 17:58:46 +0200 wenzelm tuned;
Fri, 30 Jul 1999 13:43:26 +0200 wenzelm eliminated METHOD0 in favour of same_tac;
Sun, 29 Nov 1998 13:13:57 +0100 wenzelm method brute_force = ALLGOALS force_tac;
Wed, 18 Nov 1998 11:01:48 +0100 wenzelm method setup;
Fri, 23 Oct 1998 20:35:56 +0200 oheimb corrected auto_tac (applications of unsafe wrappers)
Fri, 25 Sep 1998 14:06:00 +0200 paulson deleted illegal "op"
Thu, 24 Sep 1998 17:17:56 +0200 oheimb removed addcongs2 and delcongs2
Mon, 21 Sep 1998 23:17:28 +0200 oheimb improved addbefore and addSbefore
Fri, 11 Sep 1998 17:20:58 +0200 oheimb added clarsimp_tac and Clarsimp_tac
Thu, 30 Jul 1998 19:02:52 +0200 wenzelm functorized Clasimp module;
Sat, 02 May 1998 16:46:17 +0200 wenzelm added CLASIMPSET(') tacticals;
Fri, 01 May 1998 22:30:42 +0200 oheimb Auto_tac: now uses enhanced version of asm_full_simp_tac,
Tue, 10 Mar 1998 18:26:27 +0100 oheimb renamed smart_tac to force_tac, slight improvement of force_tac
Thu, 26 Feb 1998 15:45:33 +0100 oheimb added smart_tac
Wed, 25 Feb 1998 20:25:27 +0100 oheimb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
less more (0) tip