| Tue, 16 May 2023 14:30:32 +0200 |
wenzelm |
support for context within morphism (for background theory);
|
file |
diff |
annotate
|
| Mon, 15 May 2023 14:13:58 +0200 |
wenzelm |
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 02 May 2023 11:11:19 +0200 |
wenzelm |
proper checks;
|
file |
diff |
annotate
|
| Mon, 18 Oct 2021 11:40:57 +0200 |
wenzelm |
more robust Variable.revert_bounds (see also b12f2cef3ee5);
|
file |
diff |
annotate
|
| Sat, 16 Oct 2021 20:21:13 +0200 |
wenzelm |
more accurate treatment of context;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 23:07:02 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 12:33:14 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 11:32:18 +0200 |
wenzelm |
more efficient operations: traverse hyps only when required;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2021 23:21:32 +0200 |
wenzelm |
more robust signature: result has no particular order;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 22:17:15 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 04 Sep 2021 18:21:58 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2021 18:57:33 +0200 |
wenzelm |
more scalable data structure (but: rarely used many arguments);
|
file |
diff |
annotate
|
| Thu, 26 Aug 2021 14:52:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2021 14:45:19 +0200 |
wenzelm |
more scalable data structure (but: rarely used with > 5 arguments);
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Thu, 19 Dec 2019 14:46:10 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 12 Oct 2019 13:43:17 +0200 |
wenzelm |
more compact XML: separate environment for free variables;
|
file |
diff |
annotate
|
| Thu, 19 Sep 2019 10:52:18 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 21:47:54 +0200 |
wenzelm |
more structural integrity;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 13:28:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 15:55:36 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 23:31:10 +0200 |
wenzelm |
highlighting of entity def/ref positions wrt. cursor;
|
file |
diff |
annotate
|
| Mon, 11 Apr 2016 15:50:18 +0200 |
wenzelm |
back to dummy constraints (amending dd2914250ca7): important for Syntax_Phases.get_free/is_declared;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 22:00:55 +0200 |
wenzelm |
more accurate mixfix type constraints;
|
file |
diff |
annotate
|
| Thu, 31 Dec 2015 15:27:25 +0100 |
wenzelm |
more precise context -- potentially relevant for Eisbach dummy thm;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 16:29:39 +0100 |
wenzelm |
suppress irrelevant position reports;
|
file |
diff |
annotate
|
| Wed, 23 Dec 2015 20:23:44 +0100 |
wenzelm |
clarified context policy to allow multiple dummies;
|
file |
diff |
annotate
|
| Fri, 23 Oct 2015 17:17:11 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 21:10:41 +0200 |
wenzelm |
clarified Variable.gen_all;
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 20:59:39 +0200 |
wenzelm |
more explicit context;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 23:40:39 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jul 2015 22:36:31 +0200 |
wenzelm |
SUBPROOF and Subgoal.FOCUS combinators use anonymous quasi-bound variables (like the Simplifier);
|
file |
diff |
annotate
|
| Wed, 08 Jul 2015 19:28:43 +0200 |
wenzelm |
Variable.focus etc.: optional bindings provided by user;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Tue, 09 Jun 2015 11:51:05 +0200 |
wenzelm |
clarified term bindings;
|
file |
diff |
annotate
|
| Wed, 03 Jun 2015 19:25:05 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 20:18:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 20:07:37 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 21:58:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 28 Mar 2015 17:26:42 +0100 |
wenzelm |
prefer Variable.focus, despite subtle differences of Logic.strip_params vs. Term.strip_all_vars;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 16:17:07 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 24 Mar 2015 15:57:51 +0100 |
wenzelm |
admit dummy patterns in instantiations;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 22:57:04 +0100 |
wenzelm |
implicit goal parameters are improper;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 15:40:36 +0100 |
wenzelm |
added declare_maxidx operations for Eisbach;
|
file |
diff |
annotate
|
| Sat, 07 Mar 2015 12:32:55 +0100 |
wenzelm |
clarified Variable.export: observe maxidx of target context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 17:32:20 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 13:28:04 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Sun, 21 Dec 2014 22:49:17 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:36:50 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|