author wenzelm Sat, 28 Jul 2007 20:40:18 +0200 changeset 24016 cf022cc710ae parent 24015 253720dddcde child 24017 363287741ebe
--- 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 +
;