src/Pure/Isar/expression.ML
Fri, 22 Dec 2023 21:03:16 +0100 wenzelm clarified signature: downgrade old-style Global_Theory.add_defs to Global_Theory.add_def without attributes;
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, 23 May 2023 18:46:15 +0200 wenzelm tuned signature: more position information;
Thu, 18 May 2023 23:20:41 +0200 wenzelm tuned;
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);
Mon, 15 May 2023 20:55:17 +0200 wenzelm clarified signature;
Sun, 14 May 2023 13:15:21 +0200 wenzelm tuned;
Sun, 14 May 2023 13:00:49 +0200 wenzelm proper Thm.trim_context / Thm.transfer;
Fri, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Thu, 09 Sep 2021 22:29:15 +0200 wenzelm clarified order of extra type variables, following names more often than occurrences;
Thu, 09 Sep 2021 22:12:05 +0200 wenzelm clarified signature;
Thu, 09 Sep 2021 21:44:11 +0200 wenzelm tuned;
Thu, 09 Sep 2021 21:37:42 +0200 wenzelm more scalable operations;
Thu, 09 Sep 2021 21:14:05 +0200 wenzelm omit obsolete field "xs": originally from fd0f8fa2b6bd, but later unused;
Thu, 09 Sep 2021 12:33:14 +0200 wenzelm clarified signature;
Fri, 03 Sep 2021 18:57:33 +0200 wenzelm more scalable data structure (but: rarely used many arguments);
Sun, 15 Nov 2020 07:17:05 +0000 haftmann type alias for mixin bundles
Sun, 01 Nov 2020 16:54:49 +0100 haftmann bundle mixins for locale and class specifications
Tue, 26 Nov 2019 08:09:44 +0100 ballarin Remove diagnostic command 'print_dependencies'.
Mon, 04 Nov 2019 15:06:54 +0100 wenzelm prefer named result;
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;
Wed, 28 Aug 2019 19:19:17 +0200 ballarin Integrate locale activation fallback diagnostics with 'trace_locales'.
Tue, 04 Jun 2019 13:08:05 +0200 wenzelm proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
Mon, 03 Jun 2019 15:40:08 +0200 wenzelm clarified signature;
Mon, 24 Sep 2018 19:34:14 +0200 wenzelm tuned signature: prefer value-oriented pretty-printing;
Fri, 31 Aug 2018 13:34:31 +0200 wenzelm tuned;
Fri, 02 Mar 2018 15:14:59 +0100 ballarin Drop illegitimate optimisation from d5a7f2c54655.
Fri, 02 Mar 2018 14:28:39 +0100 ballarin Fall back to reading rewrite morphism first if activation fails without it.
Fri, 02 Mar 2018 14:19:25 +0100 ballarin Proper rewrite morphisms in locale instances.
Fri, 23 Feb 2018 21:12:08 +0100 wenzelm tuned signature;
Fri, 23 Feb 2018 20:55:46 +0100 wenzelm tuned signature;
Wed, 21 Feb 2018 20:13:42 +0100 wenzelm more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;
Wed, 21 Feb 2018 16:26:42 +0100 wenzelm minor tuning and clarification;
Tue, 20 Feb 2018 23:23:40 +0100 wenzelm minor tuning and clarification;
Tue, 20 Feb 2018 23:03:28 +0100 wenzelm tuned signature;
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 15:41:17 +0100 wenzelm tuned;
Tue, 16 Jan 2018 19:28:05 +0100 ballarin Experimental support for rewrite morphisms in locale instances.
Fri, 04 Aug 2017 08:12:37 +0200 haftmann provide explicit variant initializers for regular named target vs. almost-named target
Wed, 06 Jul 2016 11:29:51 +0200 wenzelm tuned signature;
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;
Thu, 12 May 2016 10:57:09 +0200 wenzelm avoid spurious fact index, notably in "context begin" (via Bundle.context);
Thu, 12 May 2016 10:21:59 +0200 wenzelm tuned;
Thu, 12 May 2016 10:16:52 +0200 wenzelm tuned;
Tue, 12 Apr 2016 14:38:57 +0200 wenzelm Type_Infer.object_logic controls improvement of type inference result;
Tue, 29 Mar 2016 21:17:29 +0200 wenzelm more position information for type mixfix;
Sat, 14 Nov 2015 08:45:51 +0100 haftmann separate ML module for interpretation
Tue, 06 Oct 2015 13:31:44 +0200 wenzelm just one theorem kind, which is legacy anyway;
Wed, 02 Sep 2015 16:01:57 +0200 wenzelm expose locale definition to normal user-namespace (for completion, query etc.) -- in contrast to 149f80f27c84, ba9f52f56356, f7d9c5e5d2f9;
Sun, 16 Aug 2015 19:25:08 +0200 wenzelm added Thm.chyps_of;
Thu, 13 Aug 2015 11:05:19 +0200 wenzelm tuned signature, in accordance to sortBy in Scala;
Sun, 14 Jun 2015 23:22:08 +0200 wenzelm improved treatment of Element.Obtains via Expression.prepare_stmt;
Sun, 14 Jun 2015 20:10:21 +0200 wenzelm clarified context;
Tue, 09 Jun 2015 16:42:17 +0200 wenzelm tuned signature;
Sun, 07 Jun 2015 20:03:40 +0200 wenzelm tuned signature;
Wed, 08 Apr 2015 19:39:08 +0200 wenzelm proper context for Object_Logic operations;
less more (0) -100 -60 tip