src/Pure/raw_simplifier.ML
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, 12 Dec 2013 22:38:25 +0100 wenzelm clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
Thu, 12 Dec 2013 21:14:33 +0100 wenzelm generic trace operations for main steps of Simplifier;
Thu, 12 Dec 2013 17:34:50 +0100 wenzelm tuned signature;
Thu, 12 Dec 2013 16:56:53 +0100 wenzelm tuned whitespace;
Thu, 12 Dec 2013 16:17:35 +0100 wenzelm tuned whitespace;
Thu, 12 Dec 2013 14:35:31 +0100 wenzelm removed dead code -- ctxt is never visible (see also 658fcba35ed7);
Thu, 30 May 2013 13:07:23 +0200 wenzelm tuned signature;
Mon, 20 May 2013 20:49:10 +0200 wenzelm more rigorous check of simplifier context;
Mon, 20 May 2013 14:04:21 +0200 wenzelm tuned;
Thu, 16 May 2013 17:39:38 +0200 wenzelm tuned signature -- depend on context by default;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Thu, 04 Apr 2013 10:30:28 +0200 nipkow removed unnerving (esp in jedit) and pointless warning
Sat, 30 Mar 2013 17:27:21 +0100 wenzelm amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;
Sat, 30 Mar 2013 17:13:21 +0100 wenzelm more formal cong_name;
Sat, 29 Sep 2012 18:23:46 +0200 wenzelm more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
Sat, 31 Mar 2012 19:26:23 +0200 wenzelm tuned signature;
Mon, 27 Feb 2012 15:42:07 +0100 wenzelm eliminated odd comment from distant past;
Tue, 14 Feb 2012 19:29:54 +0100 wenzelm tuned signature;
Tue, 14 Feb 2012 17:51:29 +0100 wenzelm eliminated unused rewrite_goal_rule;
Tue, 14 Feb 2012 17:26:35 +0100 wenzelm eliminated obsolete aliases;
Wed, 11 Jan 2012 16:25:34 +0100 wenzelm more qualified names;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 23 Nov 2011 23:07:59 +0100 wenzelm tuned;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Tue, 08 Nov 2011 12:03:51 +0100 wenzelm eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);
Fri, 28 Oct 2011 17:15:52 +0200 wenzelm tuned signature -- refined terminology;
Mon, 08 Aug 2011 17:23:15 +0200 wenzelm misc tuning -- eliminated old-fashioned rep_thm;
Wed, 29 Jun 2011 21:34:16 +0200 wenzelm tuned signature;
Wed, 29 Jun 2011 20:39:41 +0200 wenzelm simplified/unified Simplifier.mk_solver;
Thu, 09 Jun 2011 17:51:49 +0200 wenzelm simplified Name.variant -- discontinued builtin fold_map;
Fri, 22 Apr 2011 13:07:47 +0200 wenzelm tuned signature;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Sat, 08 Jan 2011 14:30:54 +0100 wenzelm tuned;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
less more (0) tip