changeset 17259 dda237f1d299
parent 17228 19b460b39dad
child 17269 c5a52602c4a7
--- a/NEWS	Mon Sep 05 16:47:28 2005 +0200
+++ b/NEWS	Mon Sep 05 17:38:15 2005 +0200
@@ -93,6 +93,15 @@
 document practical applications.  The ML antiquotation prints
 type-checked ML expressions verbatim.
+* Markup commands 'chapter', 'section', 'subsection', 'subsubsection',
+and 'text' support optional locale specification '(in loc)', which
+specifies the default context for interpreting antiquotations.
+For example: 'text (in LC) {* @{thm fold_cummute}*}'.
+* Option 'locale=NAME' of antiquotations specifies an alternative
+context interpreting the subsequent argument.  For example: @{thm
+[locale=LC] fold_commute}.
 * Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
 a proof context.
@@ -257,10 +266,6 @@
 statements with 'includes'.  INCOMPATIBILITY: produces a different
 theorem statement in rare situations.
-* Antiquotations provide the option 'locale=NAME' to specify an
-alternative context used for evaluating and printing the subsequent
-argument, as in @{thm [locale=LC] fold_commute}, for example.
 * Locale inspection command 'print_locale' omits notes elements.  Use
 'print_locale!' to have them included in the output.