# HG changeset patch
# User ballarin
# Date 1226324209 -3600
# Node ID 08314d96246b3f49d11056fe2638d8ab6fd85ddf
# Parent  185110a4b97a6d2d2b557cbd31e1221ba4c19d73
Made doc compatible with the system.

diff -r 185110a4b97a -r 08314d96246b doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Mon Nov 10 09:03:28 2008 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Nov 10 14:36:49 2008 +0100
@@ -381,11 +381,7 @@
   include arbitrary declarations in any attribute specifications
   included here, e.g.\ a local @{attribute simp} rule.
 
-  \item [@{element "includes"}~@{text c}] copies the specified context
-  in a statically scoped manner.  Only available in the long goal
-  format of \secref{sec:goals}.
-
-  In contrast, the initial @{text import} specification of a locale
+  The initial @{text import} specification of a locale
   expression maintains a dynamic relation to the locales being
   referenced (benefiting from any later fact declarations in the
   obvious manner).
@@ -433,10 +429,9 @@
   loc.intro} introduction rules and therefore does not decend to
   assumptions, @{method unfold_locales} is more aggressive and applies
   @{text loc_axioms.intro} as well.  Both methods are aware of locale
-  specifications entailed by the context, both from target and
-  @{element "includes"} statements, and from interpretations (see
-  below).  New goals that are entailed by the current context are
-  discharged automatically.
+  specifications entailed by the context, both from target statements,
+  and from interpretations (see below).  New goals that are entailed
+  by the current context are discharged automatically.
 
   \end{descr}
 *}
diff -r 185110a4b97a -r 08314d96246b doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 10 09:03:28 2008 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 10 14:36:49 2008 +0100
@@ -397,11 +397,7 @@
   include arbitrary declarations in any attribute specifications
   included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
 
-  \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context
-  in a statically scoped manner.  Only available in the long goal
-  format of \secref{sec:goals}.
-
-  In contrast, the initial \isa{import} specification of a locale
+  The initial \isa{import} specification of a locale
   expression maintains a dynamic relation to the locales being
   referenced (benefiting from any later fact declarations in the
   obvious manner).
@@ -446,10 +442,9 @@
   theory.  While \hyperlink{method.intro-locales}{\mbox{\isa{intro{\isacharunderscore}locales}}} only applies the \isa{loc{\isachardot}intro} introduction rules and therefore does not decend to
   assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
   \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well.  Both methods are aware of locale
-  specifications entailed by the context, both from target and
-  \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see
-  below).  New goals that are entailed by the current context are
-  discharged automatically.
+  specifications entailed by the context, both from target statements,
+  and from interpretations (see below).  New goals that are entailed
+  by the current context are discharged automatically.
 
   \end{descr}%
 \end{isamarkuptext}%