# HG changeset patch
# User wenzelm
# Date 1185653971 -7200
# Node ID 386f025be266871363d83c6ca9251a14e59af7f0
# Parent  b3d7eb6f535f09595d79679ee1f44e301b50309a
tuned;

diff -r b3d7eb6f535f -r 386f025be266 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Sat Jul 28 22:17:46 2007 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sat Jul 28 22:19:31 2007 +0200
@@ -366,9 +366,9 @@
 not stored within the theorem database of the theory or proof context,
 but any given attributes are applied nonetheless.
 
-An attribute declaration with an extra pair of brackets --- such as
-``$[[simproc~a]]$'' --- abbreviates a theorem reference that involves
-an internal dummy fact, which will be ignored later on.  So only the
+An extra pair of brackets around attribute declarations --- such as
+``$[[simproc~a]]$'' --- abbreviates a theorem reference involving an
+internal dummy fact, which will be ignored later on.  So only the
 effect of the attribute on the background context will persist.  This
 form of in-place declarations is particularly useful with commands
 like $\DECLARE$ and $\USINGNAME$.