# HG changeset patch
# User wenzelm
# Date 1125935368 -7200
# Node ID c5a52602c4a791ae49f6da84025b2d0c9842646a
# Parent  309288714d9d32860b273a087e22f4e5f5c0fa39
tuned;

diff -r 309288714d9d -r c5a52602c4a7 NEWS
--- 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.