| 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
|
| Sat, 04 Sep 2021 22:05:35 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 03 Aug 2021 13:08:23 +0200 |
wenzelm |
more uniform signatures in ML and Scala;
|
file |
diff |
annotate
|
| Mon, 19 Aug 2019 19:12:44 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2019 21:38:42 +0200 |
wenzelm |
maintain thm_name vs. derivation_id for global facts;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2019 14:01:51 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2019 11:40:13 +0200 |
wenzelm |
clarified treatment of individual theorems;
|
file |
diff |
annotate
|
| Fri, 16 Aug 2019 10:33:25 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2018 16:08:04 +0200 |
wenzelm |
eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;
|
file |
diff |
annotate
|
| Tue, 20 Feb 2018 14:02:36 +0100 |
wenzelm |
avoid premature Lazy.force due to strict "?" operator;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 18:01:36 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 14:26:37 +0100 |
wenzelm |
store facts as lazy values;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 04 Jul 2016 11:11:19 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2016 14:42:47 +0200 |
wenzelm |
position information for literal facts;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2016 21:13:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 10 May 2016 22:25:06 +0200 |
wenzelm |
find dynamic facts as well, but static ones are preferred;
|
file |
diff |
annotate
|
| Sun, 30 Aug 2015 17:34:29 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
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
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 16:20:14 +0200 |
wenzelm |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
file |
diff |
annotate
|
| Sun, 10 Aug 2014 19:44:20 +0200 |
wenzelm |
support aliases within the facts space;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 11:22:25 +0100 |
wenzelm |
more explicit treatment of verbose mode, which includes concealed entries;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 10:08:36 +0100 |
wenzelm |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 12:28:35 +0100 |
wenzelm |
minor tuning -- NB: props are usually empty for global facts;
|
file |
diff |
annotate
|
| Mon, 10 Mar 2014 13:55:03 +0100 |
wenzelm |
abstract type Name_Space.table;
|
file |
diff |
annotate
|
| Sun, 09 Mar 2014 17:07:45 +0100 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|