1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 22:36:30 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 22:44:40 2008 +0100
     1.3 @@ -287,7 +287,7 @@
     1.4  
     1.5    \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
     1.6    \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
     1.7 -  \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
     1.8 +  \indexisarelem{defines}\indexisarelem{notes}
     1.9    \begin{rail}
    1.10      'locale' name ('=' localeexpr)? 'begin'?
    1.11      ;
    1.12 @@ -311,8 +311,6 @@
    1.13      ;
    1.14      notes: 'notes' (thmdef? thmrefs + 'and')
    1.15      ;
    1.16 -    includes: 'includes' contextexpr
    1.17 -    ;
    1.18    \end{rail}
    1.19  
    1.20    \begin{description}
    1.21 @@ -371,14 +369,9 @@
    1.22    include arbitrary declarations in any attribute specifications
    1.23    included here, e.g.\ a local @{attribute simp} rule.
    1.24  
    1.25 -  \item @{element "includes"}~@{text c} copies the specified context
    1.26 -  in a statically scoped manner.  Only available in the long goal
    1.27 -  format of \secref{sec:goals}.
    1.28 -
    1.29 -  In contrast, the initial @{text import} specification of a locale
    1.30 -  expression maintains a dynamic relation to the locales being
    1.31 -  referenced (benefiting from any later fact declarations in the
    1.32 -  obvious manner).
    1.33 +  The initial @{text import} specification of a locale expression
    1.34 +  maintains a dynamic relation to the locales being referenced
    1.35 +  (benefiting from any later fact declarations in the obvious manner).
    1.36  
    1.37    \end{description}
    1.38    
    1.39 @@ -423,10 +416,9 @@
    1.40    loc.intro} introduction rules and therefore does not decend to
    1.41    assumptions, @{method unfold_locales} is more aggressive and applies
    1.42    @{text loc_axioms.intro} as well.  Both methods are aware of locale
    1.43 -  specifications entailed by the context, both from target and
    1.44 -  @{element "includes"} statements, and from interpretations (see
    1.45 -  below).  New goals that are entailed by the current context are
    1.46 -  discharged automatically.
    1.47 +  specifications entailed by the context, both from target statements,
    1.48 +  and from interpretations (see below).  New goals that are entailed
    1.49 +  by the current context are discharged automatically.
    1.50  
    1.51    \end{description}
    1.52  *}