| changeset 26188 | 9cb1b484fe96 |
| parent 26180 | cc85eaab20f6 |
| child 26197 | 46e63f49c946 |
--- a/NEWS Sat Mar 01 14:10:13 2008 +0100 +++ b/NEWS Sat Mar 01 14:10:14 2008 +0100 @@ -112,6 +112,9 @@ *** ML *** +* ML within Isar: antiquotation @{const name} or @{const +name(typargs)} produces statically-checked Const term. + * The ``print mode'' is now a thread-local value derived from a global template (the former print_mode reference), thus access becomes non-critical. The global print_mode reference is for session