--- a/NEWS Mon Sep 05 17:38:25 2005 +0200
+++ b/NEWS Mon Sep 05 17:49:28 2005 +0200
@@ -95,12 +95,12 @@
* 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}*}'.
+specifies the default context for interpreting antiquotations. For
+example: 'text (in lattice) {* @{thm inf_assoc}*}'.
* Option 'locale=NAME' of antiquotations specifies an alternative
context interpreting the subsequent argument. For example: @{thm
-[locale=LC] fold_commute}.
+[locale=lattice] inf_assoc}.
* Proper output of proof terms (@{prf ...} and @{full_prf ...}) within
a proof context.