src/Pure/variable.ML
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);
Tue, 02 May 2023 11:11:19 +0200 wenzelm proper checks;
Mon, 18 Oct 2021 11:40:57 +0200 wenzelm more robust Variable.revert_bounds (see also b12f2cef3ee5);
Sat, 16 Oct 2021 20:21:13 +0200 wenzelm more accurate treatment of context;
Fri, 15 Oct 2021 19:25:31 +0200 wenzelm discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
Fri, 10 Sep 2021 14:59:19 +0200 wenzelm clarified signature: more scalable operations;
Thu, 09 Sep 2021 23:07:02 +0200 wenzelm more scalable operations;
Thu, 09 Sep 2021 12:33:14 +0200 wenzelm clarified signature;
Mon, 06 Sep 2021 11:32:18 +0200 wenzelm more efficient operations: traverse hyps only when required;
Sun, 05 Sep 2021 23:21:32 +0200 wenzelm more robust signature: result has no particular order;
Sat, 04 Sep 2021 22:17:15 +0200 wenzelm tuned signature;
Sat, 04 Sep 2021 21:25:08 +0200 wenzelm clarified signature;
Sat, 04 Sep 2021 18:21:58 +0200 wenzelm more scalable operations;
Fri, 03 Sep 2021 18:57:33 +0200 wenzelm more scalable data structure (but: rarely used many arguments);
Thu, 26 Aug 2021 14:52:15 +0200 wenzelm tuned;
Thu, 26 Aug 2021 14:45:19 +0200 wenzelm more scalable data structure (but: rarely used with > 5 arguments);
Thu, 19 Dec 2019 15:22:35 +0100 wenzelm more robust bound_fixes: external name does appear in "fixes" name space and could clash with direct fixes (e.g. via Subgoal.FOCUS within a global context);
Thu, 19 Dec 2019 14:46:10 +0100 wenzelm tuned signature;
Sat, 12 Oct 2019 13:43:17 +0200 wenzelm more compact XML: separate environment for free variables;
Thu, 19 Sep 2019 10:52:18 +0200 wenzelm clarified modules;
Tue, 20 Aug 2019 11:01:05 +0200 wenzelm clarified signature;
Mon, 03 Jun 2019 21:47:54 +0200 wenzelm more structural integrity;
Mon, 03 Jun 2019 15:40:08 +0200 wenzelm clarified signature;
Mon, 03 Jun 2019 13:28:01 +0200 wenzelm tuned signature;
Thu, 03 Jan 2019 15:55:36 +0100 wenzelm tuned signature;
Thu, 03 Jan 2019 14:12:44 +0100 wenzelm clarified signature: more types;
Sun, 25 Feb 2018 15:44:46 +0100 wenzelm eliminated ASCII syntax from Pure bootstrap;
Tue, 13 Dec 2016 11:51:42 +0100 wenzelm more symbols;
Thu, 14 Apr 2016 23:31:10 +0200 wenzelm highlighting of entity def/ref positions wrt. cursor;
Mon, 11 Apr 2016 15:50:18 +0200 wenzelm back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;
less more (0) -100 -50 -30 tip