--- 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$.