| Sun, 23 Sep 2018 19:59:53 +0200 |
wenzelm |
discontinued old-style inner comments;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 14:11:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 14:02:37 +0100 |
wenzelm |
more efficient tokens_match_ord based on token_kind_index;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:49:56 +0100 |
wenzelm |
more abstract type;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:40:26 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:26:50 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:23:53 +0100 |
wenzelm |
explicit dummy token;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:18:36 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 31 Jan 2018 11:09:05 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2018 18:38:18 +0100 |
wenzelm |
tuned data structure and operations;
|
file |
diff |
annotate
|
| Tue, 30 Jan 2018 11:48:38 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2018 19:28:52 +0100 |
wenzelm |
clarified take/drop/chop prefix/suffix;
|
file |
diff |
annotate
|
| Mon, 15 Jan 2018 23:03:01 +0100 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
| Sun, 14 Jan 2018 15:06:27 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 14 Jan 2018 14:11:02 +0100 |
wenzelm |
clarified modules: uniform notion of formal comments;
|
file |
diff |
annotate
|
| Sat, 13 Jan 2018 11:22:46 +0100 |
wenzelm |
added \<^cancel> operator for unused text;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2018 20:19:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 09 Jan 2018 17:09:34 +0100 |
wenzelm |
clarified markup: more like outer syntax side-comment;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2018 21:28:03 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sun, 07 Jan 2018 15:12:00 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 06 Jan 2018 16:56:07 +0100 |
wenzelm |
inner syntax comments may be written as "\<comment> \<open>text\<close>";
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 15:46:51 +0200 |
wenzelm |
accomodate Poly/ML repository version, which treats singleton strings as boxed;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2016 16:23:25 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 20:53:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 06 Mar 2016 16:19:02 +0100 |
wenzelm |
clarified treatment of fragments of Isabelle symbols during bootstrap;
|
file |
diff |
annotate
|
| Sun, 18 Oct 2015 21:30:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 29 Dec 2014 15:38:59 +0100 |
wenzelm |
more toplevel pretty printing;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 22:02:49 +0100 |
wenzelm |
discontinued obsolete \<^sync> marker;
|
file |
diff |
annotate
|