src/Pure/General/name_space.ML
Mon, 08 May 2023 11:09:13 +0200 wenzelm tuned whitespace;
Sun, 07 May 2023 14:25:41 +0200 wenzelm tuned comments;
Sun, 07 May 2023 14:24:22 +0200 wenzelm tuned;
Sun, 07 May 2023 14:18:48 +0200 wenzelm hide names more thorougly, in contrast to 1d82061fbb12 and 00e9ca1e7261: e.g. relevant for overlapping accesses seen in 'inductive_set';
Sat, 06 May 2023 23:20:20 +0200 wenzelm back to more elementary concept of aliases as adhoc change of accesses, but now with "suppress" information (see also 31ea5c1f874d);
Sat, 06 May 2023 14:49:54 +0200 wenzelm tuned;
Sat, 06 May 2023 14:46:41 +0200 wenzelm clarified data representation: slightly more compact, since internals_hidden is sparesely populated and rarely changes;
Fri, 05 May 2023 23:03:48 +0200 wenzelm unused;
Fri, 05 May 2023 22:57:10 +0200 wenzelm more complete accesses for "extern" operation, notably for aliases;
Fri, 05 May 2023 15:56:12 +0200 wenzelm more explicit entries for aliases, with proper checks in "strict" mode (e.g. for logical entities);
Fri, 05 May 2023 12:34:23 +0200 wenzelm tuned;
Fri, 05 May 2023 12:17:29 +0200 wenzelm tuned;
Fri, 05 May 2023 12:01:09 +0200 wenzelm clarified signature;
Thu, 04 May 2023 17:29:54 +0200 wenzelm tuned;
Thu, 04 May 2023 11:42:04 +0200 wenzelm more accurate treatment of traditional name space accesses (refining 948f5dc4d694, fcd85e04a948, 238307775d52);
Wed, 03 May 2023 23:11:12 +0200 wenzelm tuned;
Wed, 03 May 2023 11:34:47 +0200 wenzelm proper treatment of restriction (for 'qualified');
Tue, 02 May 2023 23:22:30 +0200 wenzelm misc tuning;
Tue, 02 May 2023 22:33:07 +0200 wenzelm more complete accesses for hide operation (amending fcd85e04a948), e.g. relevant for AFP/thys/Jordan_Normal_Form/Matrix_Kernel.thy in AFP/4d8afd37b465;
Tue, 02 May 2023 14:19:34 +0200 wenzelm minor performance tuning: more compact representation of only sparsely table;
Tue, 02 May 2023 11:38:53 +0200 wenzelm minor performance tuning: no storage of accesses, produce Binding.full_name_spec on the spot;
Tue, 02 May 2023 11:11:19 +0200 wenzelm proper checks;
Tue, 02 May 2023 10:49:38 +0200 wenzelm tuned;
Tue, 02 May 2023 10:32:04 +0200 wenzelm tuned structure;
Tue, 02 May 2023 10:13:02 +0200 wenzelm tuned;
Mon, 01 May 2023 22:47:51 +0200 wenzelm clarified extern vs. alias/hide: output alternative names, if possible;
Mon, 01 May 2023 22:19:01 +0200 wenzelm tuned;
Wed, 26 Apr 2023 15:38:49 +0200 wenzelm tuned signature;
Sat, 15 Apr 2023 22:26:22 +0200 wenzelm tuned;
Sat, 15 Apr 2023 13:52:06 +0200 wenzelm tuned signature;
Fri, 14 Apr 2023 16:01:00 +0200 wenzelm proforma use of Long_Name.chunks, without change of the representation of accesses yet;
Thu, 13 Apr 2023 23:08:39 +0200 wenzelm clarified signature;
Wed, 12 Apr 2023 15:22:52 +0200 wenzelm misc tuning and clarification;
Wed, 12 Apr 2023 12:57:10 +0200 wenzelm more compact: avoid redundant entries;
Wed, 12 Apr 2023 11:27:11 +0200 wenzelm tuned;
Wed, 12 Apr 2023 11:25:50 +0200 wenzelm tuned;
Tue, 11 Apr 2023 11:16:33 +0200 wenzelm minor performance tuning: more compact persistent data;
Tue, 11 Apr 2023 09:54:46 +0200 wenzelm unused (see 34dd96a06c45);
Fri, 26 Aug 2022 12:38:00 +0200 wenzelm removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
Fri, 12 Nov 2021 13:02:20 +0100 wenzelm clarified properties: avoid empty entry;
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots;
Tue, 07 Sep 2021 22:35:44 +0200 wenzelm more markup, e.g. to locate defining theory node in formal document output;
Tue, 07 Sep 2021 21:47:50 +0200 wenzelm tuned signature;
Tue, 07 Sep 2021 21:16:22 +0200 wenzelm export other entities, e.g. relevant for formal document output;
Tue, 24 Aug 2021 14:56:55 +0200 wenzelm clarified signature;
Fri, 17 Jul 2020 14:56:55 +0200 wenzelm prefer conservative extend/merge of theory naming;
Fri, 03 Apr 2020 13:51:56 +0200 wenzelm more accurate context position reports;
Mon, 09 Dec 2019 11:17:34 +0100 wenzelm clarified signature: store full theory name;
Tue, 20 Aug 2019 11:01:05 +0200 wenzelm clarified signature;
Thu, 03 Jan 2019 14:12:44 +0100 wenzelm clarified signature: more types;
Mon, 12 Nov 2018 15:14:12 +0100 wenzelm clarified signature;
Thu, 25 Oct 2018 15:41:40 +0200 wenzelm proper completion for @{named_theorems};
Sun, 13 May 2018 15:05:21 +0200 wenzelm more operations;
Mon, 03 Jul 2017 14:24:55 +0200 wenzelm complete on long name components as well;
Mon, 03 Jul 2017 09:57:26 +0200 wenzelm tuned;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Tue, 18 Oct 2016 17:41:56 +0200 wenzelm replaced inefficient valid_accesses by is_valid_access, based on stored input accesses: e.g. relevant for Proof_Context.update_thms;
Mon, 06 Jun 2016 10:34:56 +0200 wenzelm less redundant exploration of full name space;
Mon, 06 Jun 2016 08:36:03 +0200 wenzelm tuned;
Sun, 17 Apr 2016 20:11:02 +0200 wenzelm clarified signature;
less more (0) -100 -60 tip