1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Mon Nov 10 09:03:28 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Mon Nov 10 14:36:49 2008 +0100
     1.3 @@ -381,11 +381,7 @@
     1.4    include arbitrary declarations in any attribute specifications
     1.5    included here, e.g.\ a local @{attribute simp} rule.
     1.6  
     1.7 -  \item [@{element "includes"}~@{text c}] copies the specified context
     1.8 -  in a statically scoped manner.  Only available in the long goal
     1.9 -  format of \secref{sec:goals}.
    1.10 -
    1.11 -  In contrast, the initial @{text import} specification of a locale
    1.12 +  The initial @{text import} specification of a locale
    1.13    expression maintains a dynamic relation to the locales being
    1.14    referenced (benefiting from any later fact declarations in the
    1.15    obvious manner).
    1.16 @@ -433,10 +429,9 @@
    1.17    loc.intro} introduction rules and therefore does not decend to
    1.18    assumptions, @{method unfold_locales} is more aggressive and applies
    1.19    @{text loc_axioms.intro} as well.  Both methods are aware of locale
    1.20 -  specifications entailed by the context, both from target and
    1.21 -  @{element "includes"} statements, and from interpretations (see
    1.22 -  below).  New goals that are entailed by the current context are
    1.23 -  discharged automatically.
    1.24 +  specifications entailed by the context, both from target statements,
    1.25 +  and from interpretations (see below).  New goals that are entailed
    1.26 +  by the current context are discharged automatically.
    1.27  
    1.28    \end{descr}
    1.29  *}

     2.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 10 09:03:28 2008 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Mon Nov 10 14:36:49 2008 +0100
     2.3 @@ -397,11 +397,7 @@
     2.4    include arbitrary declarations in any attribute specifications
     2.5    included here, e.g.\ a local \hyperlink{attribute.simp}{\mbox{\isa{simp}}} rule.
     2.6  
     2.7 -  \item [\hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}}~\isa{c}] copies the specified context
     2.8 -  in a statically scoped manner.  Only available in the long goal
     2.9 -  format of \secref{sec:goals}.
    2.10 -
    2.11 -  In contrast, the initial \isa{import} specification of a locale
    2.12 +  The initial \isa{import} specification of a locale
    2.13    expression maintains a dynamic relation to the locales being
    2.14    referenced (benefiting from any later fact declarations in the
    2.15    obvious manner).
    2.16 @@ -446,10 +442,9 @@
    2.17    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
    2.18    assumptions, \hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}} is more aggressive and applies
    2.19    \isa{loc{\isacharunderscore}axioms{\isachardot}intro} as well.  Both methods are aware of locale
    2.20 -  specifications entailed by the context, both from target and
    2.21 -  \hyperlink{element.includes}{\mbox{\isa{\isakeyword{includes}}}} statements, and from interpretations (see
    2.22 -  below).  New goals that are entailed by the current context are
    2.23 -  discharged automatically.
    2.24 +  specifications entailed by the context, both from target statements,
    2.25 +  and from interpretations (see below).  New goals that are entailed
    2.26 +  by the current context are discharged automatically.
    2.27  
    2.28    \end{descr}%
    2.29  \end{isamarkuptext}%