# HG changeset patch
# User wenzelm
# Date 1226612680 -3600
# Node ID 8ea7403147c5edffdc81429ad383b8c8e29167d1
# Parent  de95d007eaed77678763e75cb88150e630bd570e
removed "includes" element (lost update?);

diff -r de95d007eaed -r 8ea7403147c5 doc-src/IsarRef/Thy/Spec.thy
--- 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}
 *}