--- a/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 22:36:30 2008 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Thu Nov 13 22:44:40 2008 +0100
@@ -287,7 +287,7 @@
\indexouternonterm{contextexpr}\indexouternonterm{contextelem}
\indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
- \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes}
+ \indexisarelem{defines}\indexisarelem{notes}
\begin{rail}
'locale' name ('=' localeexpr)? 'begin'?
;
@@ -311,8 +311,6 @@
;
notes: 'notes' (thmdef? thmrefs + 'and')
;
- includes: 'includes' contextexpr
- ;
\end{rail}
\begin{description}
@@ -371,14 +369,9 @@
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
- expression maintains a dynamic relation to the locales being
- referenced (benefiting from any later fact declarations in the
- obvious manner).
+ 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).
\end{description}
@@ -423,10 +416,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{description}
*}