src/Pure/simplifier.ML
Mon, 03 Jun 2019 15:40:08 +0200 wenzelm clarified signature;
Fri, 04 Jan 2019 21:49:06 +0100 wenzelm support for isabelle update -u control_cartouches;
Tue, 27 Nov 2018 21:07:39 +0100 wenzelm more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
Wed, 06 Jun 2018 18:19:55 +0200 nipkow reorient -> split; documented split
Thu, 26 Apr 2018 19:51:32 +0200 nipkow new simp modifier: reorient
Thu, 01 Feb 2018 15:31:25 +0100 wenzelm clarified signature: prefer proper order operation;
Wed, 06 Dec 2017 18:59:33 +0100 wenzelm prefer control symbol antiquotations;
Wed, 06 Dec 2017 15:46:35 +0100 wenzelm more embedded cartouche arguments;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Wed, 20 Jul 2016 22:36:10 +0200 wenzelm provide Pure.simp/simp_all, which only know about meta-equality;
Thu, 02 Jun 2016 16:23:10 +0200 wenzelm avoid warnings on duplicate rules in the given list;
Fri, 08 Apr 2016 20:15:20 +0200 wenzelm eliminated unused simproc identifier;
Wed, 16 Dec 2015 16:31:36 +0100 wenzelm rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Wed, 09 Sep 2015 23:01:27 +0200 wenzelm clarified declaration flags, like 'declaration' command;
Wed, 09 Sep 2015 20:57:21 +0200 wenzelm simplified simproc programming interfaces;
Wed, 02 Sep 2015 23:31:41 +0200 wenzelm eliminated pointless cterms;
Fri, 03 Apr 2015 19:56:51 +0200 wenzelm more uniform "verbose" option to print name space;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Sun, 01 Mar 2015 23:35:41 +0100 wenzelm added Proof_Context.cterm_of/ctyp_of convenience;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Sun, 09 Nov 2014 17:04:14 +0100 wenzelm proper context for match_tac etc.;
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;
Thu, 10 Apr 2014 12:22:29 +0200 wenzelm added simproc markup, which also indicates legacy simprocs outside the name space;
Tue, 18 Mar 2014 15:29:58 +0100 wenzelm more antiquotations;
Wed, 12 Mar 2014 22:57:50 +0100 wenzelm tuned signature -- clarified module name;
Sun, 12 Jan 2014 18:34:00 +0100 wenzelm proper context for clear_simpset: preserve dounds, depth;
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;
Mon, 11 Nov 2013 20:50:12 +0100 wenzelm tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
Fri, 23 Aug 2013 20:35:50 +0200 wenzelm added Theory.setup convenience;
Wed, 26 Jun 2013 21:48:23 +0200 wenzelm less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 10 Apr 2013 17:27:38 +0200 wenzelm obsolete -- tools should refer to proper Proof.context;
Sat, 30 Mar 2013 17:13:21 +0100 wenzelm more formal cong_name;
Sat, 30 Mar 2013 13:40:19 +0100 wenzelm more item markup;
Fri, 29 Mar 2013 22:14:27 +0100 wenzelm Pretty.item markup for improved readability of lists of items;
Sat, 17 Nov 2012 17:55:52 +0100 wenzelm tuned signature;
Sat, 11 Aug 2012 22:17:46 +0200 wenzelm faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
Sat, 14 Apr 2012 17:15:57 +0200 wenzelm outermost SELECT_GOAL potentially improves performance;
Sat, 31 Mar 2012 19:26:23 +0200 wenzelm tuned signature;
Sun, 18 Mar 2012 13:04:22 +0100 wenzelm maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
Sat, 17 Mar 2012 23:55:03 +0100 wenzelm proper naming of simprocs according to actual target context;
Sat, 03 Mar 2012 21:52:15 +0100 wenzelm tuned;
Tue, 14 Feb 2012 19:29:54 +0100 wenzelm tuned signature;
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 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Sun, 06 Nov 2011 21:51:46 +0100 wenzelm more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
Thu, 03 Nov 2011 22:15:47 +0100 wenzelm tuned -- Variable.declare_term is already part of Variable.auto_fixes;
Fri, 28 Oct 2011 22:17:30 +0200 wenzelm uniform Local_Theory.declaration with explicit params;
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;
Mon, 27 Jun 2011 16:53:31 +0200 wenzelm ML antiquotations are managed as theory data, with proper name space and entity markup;
Fri, 13 May 2011 23:58:40 +0200 wenzelm clarified map_simpset versus Simplifier.map_simpset_global;
less more (0) -100 -60 tip