| Mon, 24 Sep 2018 20:05:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 19:53:45 +0200 |
wenzelm |
tuned signature: prefer value-oriented pretty-printing;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 19:43:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 19:34:14 +0200 |
wenzelm |
tuned signature: prefer value-oriented pretty-printing;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 19:06:56 +0200 |
wenzelm |
tuned (according to signature);
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 15:34:19 +0200 |
wenzelm |
tuned comments: local context is intended according to 06fd1914b902 and documentation for command 'print_interps';
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 15:20:21 +0200 |
wenzelm |
more position information;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:58:15 +0200 |
wenzelm |
clarified message;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 13:01:25 +0200 |
wenzelm |
tuned signature: more explicit types;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 12:16:19 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 12:07:17 +0200 |
wenzelm |
eliminated dead code (see b806a7678083);
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 11:50:09 +0200 |
wenzelm |
tuned signature: canonical argument order;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 11:45:20 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 21 Sep 2018 22:26:10 +0200 |
wenzelm |
clarified locale content: proper args with types for interpretation/axioms and typargs derived from the result;
|
file |
diff |
annotate
|
| Wed, 19 Sep 2018 20:45:47 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 19 Sep 2018 16:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2018 15:48:37 +0200 |
wenzelm |
export locale content;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2018 13:34:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 14:56:04 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 14:48:02 +0200 |
wenzelm |
more careful treatment position: existing facts refer to interpretation command, future facts refer to themselves (see also 4270da306442);
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 14:21:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 14:10:39 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 13:38:52 +0200 |
wenzelm |
clarified signature: explicit type Locale.registration;
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 16:59:40 +0200 |
wenzelm |
eliminated pointless special case (see also a8ee8e4884ec, c4c4c2f01723);
|
file |
diff |
annotate
|
| Sat, 10 Mar 2018 15:52:47 +0100 |
wenzelm |
workaround for occasional deadlock seen in HOL-Proofs with threads=2;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 21:12:08 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 20 Feb 2018 23:03:28 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 20 Feb 2018 16:29:37 +0100 |
wenzelm |
eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);
|
file |
diff |
annotate
|
| Tue, 20 Feb 2018 14:03:31 +0100 |
wenzelm |
use lazy notes for locale context init and later additions of facts;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 16:24:17 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 15:46:10 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 14:49:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 20:08:21 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 19:49:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 19:41:25 +0100 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 19:18:49 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2017 12:54:31 +0200 |
wenzelm |
eliminated suspicious Unicode;
|
file |
diff |
annotate
|
| Fri, 01 Sep 2017 11:33:32 +0200 |
ballarin |
Update header of locale.ML
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:37 +0200 |
haftmann |
prefer explicit datatype over implicit sum;
|
file |
diff |
annotate
|
| Sat, 24 Jun 2017 17:44:26 +0200 |
ballarin |
Improved error reporting when activating a locale instance (beyond syntax decls).
|
file |
diff |
annotate
|
| Thu, 25 Aug 2016 20:08:40 +0200 |
ballarin |
Improved error reporting when activating a locale instance.
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 12:02:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 11:40:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2016 11:14:10 +0200 |
wenzelm |
avoid massive multiplication of reports due to interpretation;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2016 15:53:12 +0200 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 21:10:45 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Dec 2015 16:36:26 +0100 |
wenzelm |
clarified type Token.src: plain token list, with usual implicit value assignment;
|
file |
diff |
annotate
|
| Sat, 21 Nov 2015 23:02:07 +0100 |
ballarin |
Clarify locale qualifiers: output and tutorial.
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 21:54:32 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 19:47:37 +0200 |
wenzelm |
more thorough transfer;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 15:49:12 +0200 |
wenzelm |
clarified vacuous binding;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 13:26:29 +0200 |
wenzelm |
trim context more thoroughly;
|
file |
diff |
annotate
|
| Wed, 02 Sep 2015 11:36:40 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 05:12:14 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 20:18:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|