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