# HG changeset patch
# User wenzelm
# Date 1185648018 -7200
# Node ID cf022cc710aeb5b99932b03fd12fe94a1eba79b4
# Parent  253720dddcdef588f6c7a56eccd315f4d3fe3df2
added [[decl]] notation;

diff -r 253720dddcde -r cf022cc710ae doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Sat Jul 28 20:40:17 2007 +0200
+++ b/doc-src/IsarRef/syntax.tex	Sat Jul 28 20:40:18 2007 +0200
@@ -349,21 +349,29 @@
   ;
 \end{rail}
 
-Theorem specifications come in several flavors: \railnonterm{axmdecl} and
-\railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal
-statements, while \railnonterm{thmdef} collects lists of existing theorems.
-Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs},
-the former requires an actual singleton result.  There are three forms of
-theorem references: (1) named facts $a$, (2) selections from named facts $a(i,
-j - k)$, or (3) literal fact propositions using $altstring$ syntax
+Theorem specifications come in several flavors: \railnonterm{axmdecl}
+and \railnonterm{thmdecl} usually refer to axioms, assumptions or
+results of goal statements, while \railnonterm{thmdef} collects lists
+of existing theorems.  Existing theorems are given by
+\railnonterm{thmref} and \railnonterm{thmrefs}, the former requires an
+actual singleton result.  There are three forms of theorem references:
+(1) named facts $a$, (2) selections from named facts $a(i, j - k)$, or
+(3) literal fact propositions using $altstring$ syntax
 $\backquote\phi\backquote$, (see also method $fact$ in
 \S\ref{sec:pure-meth-att}).
 
-Any kind of theorem specification may include lists of attributes both on the
-left and right hand sides; attributes are applied to any immediately preceding
-fact.  If names are omitted, the theorems are not stored within the theorem
-database of the theory or proof context, but any given attributes are applied
-nonetheless.
+Any kind of theorem specification may include lists of attributes both
+on the left and right hand sides; attributes are applied to any
+immediately preceding fact.  If names are omitted, the theorems are
+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
+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$.
 
 \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
 \indexouternonterm{thmdef}\indexouternonterm{thmref}
@@ -375,7 +383,7 @@
   ;
   thmdef: thmbind '='
   ;
-  thmref: (nameref selection? | altstring) attributes?
+  thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
   ;
   thmrefs: thmref +
   ;