src/Pure/Isar/element.ML
Tue, 25 Jul 2023 14:12:26 +0200 wenzelm performance tuning: prefer static simpset within functional closure of morphism (with notable impact on specifications "in" class, e.g. AFP/No_FTL_observers);
Tue, 16 May 2023 19:20:18 +0200 wenzelm more careful treatment of set_context / reset_context for persistent morphisms;
Tue, 16 May 2023 17:08:31 +0200 wenzelm clarified transfer / trim_context on persistent Token.source (e.g. attribute expressions): actually set/reset implicit context;
Tue, 16 May 2023 14:30:32 +0200 wenzelm support for context within morphism (for background theory);
Sun, 14 May 2023 13:00:49 +0200 wenzelm proper Thm.trim_context / Thm.transfer;
Tue, 18 Apr 2023 22:24:48 +0200 wenzelm tuned;
Mon, 17 Apr 2023 23:32:46 +0200 wenzelm revert b43ee37926a9 due to problems with AFP/PAPP_Impossibility;
Mon, 10 Apr 2023 22:38:18 +0200 wenzelm performance tuning: replace Ord_List by Set();
Wed, 13 Oct 2021 13:19:09 +0200 wenzelm clarified signature;
Fri, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Mon, 04 Nov 2019 14:56:49 +0100 wenzelm more robust expose_proofs corresponding to register_proofs/consolidate_theory;
Sun, 03 Nov 2019 20:38:08 +0100 wenzelm expose derivations more thoroughly, notably for locale/class reasoning;
Tue, 13 Aug 2019 10:27:21 +0200 wenzelm clarified modules;
Fri, 09 Aug 2019 17:14:49 +0200 wenzelm formal position for PThm nodes;
Mon, 03 Jun 2019 15:40:08 +0200 wenzelm clarified signature;
Fri, 25 May 2018 21:02:40 +0200 wenzelm tuned output;
Fri, 02 Mar 2018 14:19:25 +0100 ballarin Proper rewrite morphisms in locale instances.
Fri, 23 Feb 2018 13:09:45 +0100 wenzelm more robust normalization of witness, e.g. relevant for proofs of transfer_existence_ivl0, transfer_flow0 in AFP/thys/Ordinary_Differential_Equations/Numerics/Transfer_Euclidean_Space_Vector.thy;
Wed, 21 Feb 2018 20:13:42 +0100 wenzelm more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;
Mon, 19 Feb 2018 22:07:21 +0100 wenzelm support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
Mon, 19 Feb 2018 16:24:17 +0100 wenzelm clarified modules;
Sun, 28 Jan 2018 19:28:52 +0100 wenzelm clarified take/drop/chop prefix/suffix;
Tue, 25 Oct 2016 17:22:05 +0200 wenzelm more robust printing of names in the context of outer syntax;
Tue, 05 Jul 2016 14:20:27 +0200 wenzelm PIDE reports of implicit variable scope;
Thu, 23 Jun 2016 11:01:14 +0200 wenzelm tuned signature;
Mon, 21 Mar 2016 20:22:07 +0100 wenzelm more accurate fixes (e.g. for notE, FalseE), amending baa589c574ff;
Mon, 21 Mar 2016 19:57:56 +0100 wenzelm eliminated unused argument (see also 58110c1e02bc);
Thu, 07 Jan 2016 16:10:13 +0100 wenzelm prefer non-ASCII output;
Sun, 13 Dec 2015 21:56:15 +0100 wenzelm more general types Proof.method / context_tactic;
Wed, 09 Dec 2015 16:36:26 +0100 wenzelm clarified type Token.src: plain token list, with usual implicit value assignment;
Fri, 25 Sep 2015 20:37:59 +0200 wenzelm moved remaining display.ML to more_thm.ML;
Sun, 16 Aug 2015 19:25:08 +0200 wenzelm added Thm.chyps_of;
Wed, 08 Jul 2015 19:28:43 +0200 wenzelm Variable.focus etc.: optional bindings provided by user;
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Mon, 22 Jun 2015 20:36:33 +0200 wenzelm support 'when' statement, which corresponds to 'presume';
Sat, 13 Jun 2015 23:36:21 +0200 wenzelm tuned signature;
Sat, 13 Jun 2015 16:35:27 +0200 wenzelm eliminated slightly odd Element.close_form: toplevel specifications have different policies than proof text elements;
Thu, 11 Jun 2015 22:47:53 +0200 wenzelm support for 'consider' command;
Thu, 11 Jun 2015 15:44:00 +0200 wenzelm support to parse obtain clause without type-checking yet;
Thu, 11 Jun 2015 10:44:04 +0200 wenzelm tuned signature;
Wed, 10 Jun 2015 16:09:49 +0200 wenzelm clarified local after_qed: result is not exported yet;
Wed, 10 Jun 2015 14:46:31 +0200 wenzelm support for "if prems" in local goal statements;
Tue, 09 Jun 2015 16:07:11 +0200 wenzelm allow for_fixes for 'have', 'show' etc.;
Mon, 08 Jun 2015 20:53:42 +0200 wenzelm clarified Proof_Context.cert_propp/read_propp;
Sun, 07 Jun 2015 15:01:07 +0200 wenzelm tuned signature;
Sun, 03 May 2015 17:19:27 +0200 wenzelm tuned output -- avoid empty quites and extra breaks;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
Wed, 08 Apr 2015 11:52:53 +0200 wenzelm tuned signature;
Sun, 29 Mar 2015 21:58:10 +0200 wenzelm tuned signature;
Fri, 06 Mar 2015 17:32:20 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Thu, 05 Mar 2015 13:28:04 +0100 wenzelm tuned -- more explicit use of context;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Sat, 17 Jan 2015 22:52:45 +0100 wenzelm more compact content for tighter graph layout;
Thu, 30 Oct 2014 16:20:46 +0100 wenzelm eliminated aliases;
Thu, 21 Aug 2014 22:48:39 +0200 wenzelm tuned signature -- define some elementary operations earlier;
Tue, 19 Aug 2014 23:17:51 +0200 wenzelm tuned signature -- moved type src to Token, without aliases;
Tue, 19 Aug 2014 12:05:11 +0200 wenzelm simplified type Proof.method;
Tue, 05 Aug 2014 16:21:27 +0200 wenzelm clarified Element.init vs. Element.init' -- the latter also avoids redundant warnings due to declatations when preparing locale expressions / interpretations;
Sat, 08 Mar 2014 21:08:10 +0100 wenzelm modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
less more (0) -100 -60 tip