src/Pure/simplifier.ML
Wed, 18 Oct 2023 16:29:24 +0200 wenzelm clarified signature: more concise simproc setup in ML;
Tue, 17 Oct 2023 18:55:29 +0200 wenzelm support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
Sat, 27 May 2023 13:29:13 +0200 wenzelm tuned signature;
Fri, 26 May 2023 13:19:49 +0200 wenzelm clarified treatment of context;
Tue, 23 May 2023 18:46:15 +0200 wenzelm tuned signature: more position information;
Fri, 19 May 2023 11:42:12 +0200 wenzelm remove pointless context setup (see also b2e449c155a4);
Thu, 18 May 2023 17:21:29 +0200 wenzelm clarified signature: more explicit types;
Tue, 16 May 2023 19:43:42 +0200 wenzelm more standard treatment of morphism context, but hardly relevant here;
Sun, 14 May 2023 13:15:52 +0200 wenzelm tuned;
Sat, 13 May 2023 21:30:34 +0200 wenzelm tuned: avoid pointless Proof_Context.init_global of Context.proof_of;
Wed, 20 Oct 2021 20:25:33 +0200 wenzelm clarified modules;
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots;
Tue, 21 Apr 2020 07:28:17 +0000 haftmann hooks for foundational terms: protection of foundational terms during simplification
Thu, 05 Dec 2019 09:24:34 +0000 haftmann more direct accessors for simpset
Tue, 20 Aug 2019 11:01:05 +0200 wenzelm clarified signature;
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;
less more (0) -100 -60 tip