--- a/doc-src/IsarRef/Thy/Spec.thy Sun Nov 08 14:38:36 2009 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Nov 08 14:44:31 2009 +0100
@@ -257,7 +257,7 @@
\end{matharray}
\begin{rail}
- 'declaration' target? text
+ 'declaration' ('(pervasive)')? target? text
;
'declare' target? (thmrefs + 'and')
;
@@ -271,6 +271,10 @@
function is transformed according to the morphisms being involved in
the interpretation hierarchy.
+ If the @{text "(pervasive)"} option is given, the corresponding
+ declaration is applied to all possible contexts involved, including
+ the global background theory.
+
\item @{command "declare"}~@{text thms} declares theorems to the
current local theory context. No theorem binding is involved here,
unlike @{command "theorems"} or @{command "lemmas"} (cf.\