# HG changeset patch
# User wenzelm
# Date 1257687871 -3600
# Node ID 0855a09bc5cfcb6895152eac7291ceccd28121d2
# Parent  d066e8369a33cfe74288300163e7e375cafa442b
added "declaration (pervasive)";

diff -r d066e8369a33 -r 0855a09bc5cf doc-src/IsarRef/Thy/Spec.thy
--- 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.\
diff -r d066e8369a33 -r 0855a09bc5cf doc-src/IsarRef/Thy/document/Spec.tex
--- 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.\