# HG changeset patch
# User wenzelm
# Date 1427122541 -3600
# Node ID 00b62aa9f43011707542205e01e3c3b91138578e
# Parent  5d801eff5647bff27ad359f27ca25bebdffac0e7
tuned syntax diagrams -- no duplication of "target";

diff -r 5d801eff5647 -r 00b62aa9f430 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Mon Mar 23 15:55:41 2015 +0100
@@ -44,8 +44,7 @@
 
   @{rail \<open>
     (@@{command chapter} | @@{command section} | @@{command subsection} |
-      @@{command subsubsection} | @@{command text} | @@{command txt})
-      @{syntax target}? @{syntax text}
+      @@{command subsubsection} | @@{command text} | @@{command txt}) @{syntax text}
     ;
     @@{command text_raw} @{syntax text}
   \<close>}
@@ -74,7 +73,7 @@
   Except for @{command "text_raw"}, the text passed to any of the above
   markup commands may refer to formal entities via \emph{document
   antiquotations}, see also \secref{sec:antiq}. These are interpreted in the
-  present theory or proof context, or the named @{text "target"}.
+  present theory or proof context.
 
   \medskip The proof markup commands closely resemble those for theory
   specifications, but have a different formal status and produce
diff -r 5d801eff5647 -r 00b62aa9f430 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Mar 23 15:55:41 2015 +0100
@@ -99,8 +99,7 @@
 
   @{rail \<open>
     (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
-      @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
-    @{syntax target}? \<newline>
+      @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set}) \<newline>
     @{syntax "fixes"} (@'for' @{syntax "fixes"})? (@'where' clauses)? \<newline>
     (@'monos' @{syntax thmrefs})?
     ;
@@ -266,9 +265,9 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) primrec} @{syntax target}? @{syntax "fixes"} @'where' equations
+    @@{command (HOL) primrec} @{syntax "fixes"} @'where' equations
     ;
-    (@@{command (HOL) fun} | @@{command (HOL) function}) @{syntax target}? functionopts?
+    (@@{command (HOL) fun} | @@{command (HOL) function}) functionopts?
       @{syntax "fixes"} \<newline> @'where' equations
     ;
 
@@ -575,8 +574,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) partial_function} @{syntax target}?
-      '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
+    @@{command (HOL) partial_function} '(' @{syntax nameref} ')' @{syntax "fixes"} \<newline>
       @'where' @{syntax thmdecl}? @{syntax prop}
   \<close>}
 
@@ -1592,25 +1590,25 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) setup_lifting} \<newline>
-      @{syntax thmref} @{syntax thmref}? (@'parametric' @{syntax thmref})?;
+    @@{command (HOL) setup_lifting} @{syntax thmref} @{syntax thmref}? \<newline>
+      (@'parametric' @{syntax thmref})?
   \<close>}
 
   @{rail \<open>
     @@{command (HOL) lift_definition} @{syntax name} '::' @{syntax type}  @{syntax mixfix}? \<newline>
-      'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?;
+      'is' @{syntax term} (@'parametric' (@{syntax thmref}+))?
   \<close>}
 
   @{rail \<open>
-    @@{command (HOL) lifting_forget} @{syntax nameref};
+    @@{command (HOL) lifting_forget} @{syntax nameref}
   \<close>}
 
   @{rail \<open>
-    @@{command (HOL) lifting_update} @{syntax nameref};
+    @@{command (HOL) lifting_update} @{syntax nameref}
   \<close>}
 
   @{rail \<open>
-    @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?;
+    @@{attribute (HOL) lifting_restore} @{syntax thmref} (@{syntax thmref} @{syntax thmref})?
   \<close>}
 
   \begin{description}
diff -r 5d801eff5647 -r 00b62aa9f430 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Mar 23 15:55:41 2015 +0100
@@ -521,10 +521,10 @@
   entities within the current context.
 
   @{rail \<open>
-    (@@{command type_notation} | @@{command no_type_notation}) @{syntax target}?
-      @{syntax mode}? \<newline> (@{syntax nameref} @{syntax mixfix} + @'and')
+    (@@{command type_notation} | @@{command no_type_notation}) @{syntax mode}? \<newline>
+      (@{syntax nameref} @{syntax mixfix} + @'and')
     ;
-    (@@{command notation} | @@{command no_notation}) @{syntax target}? @{syntax mode}? \<newline>
+    (@@{command notation} | @@{command no_notation}) @{syntax mode}? \<newline>
       (@{syntax nameref} @{syntax mixfix} + @'and')
     ;
     @@{command write} @{syntax mode}? (@{syntax nameref} @{syntax mixfix} + @'and')
@@ -1165,6 +1165,8 @@
     @{attribute_def syntax_ast_stats} & : & @{text attribute} & default @{text false} \\
   \end{tabular}
 
+  \medskip
+
   Unlike mixfix notation for existing formal entities
   (\secref{sec:notation}), raw syntax declarations provide full access
   to the priority grammar of the inner syntax, without any sanity
diff -r 5d801eff5647 -r 00b62aa9f430 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Mon Mar 23 15:55:41 2015 +0100
@@ -432,7 +432,7 @@
   @{rail \<open>
     (@@{command lemma} | @@{command theorem} | @@{command corollary} |
      @@{command schematic_lemma} | @@{command schematic_theorem} |
-     @@{command schematic_corollary}) @{syntax target}? (goal | longgoal)
+     @@{command schematic_corollary}) (goal | longgoal)
     ;
     (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal
     ;
@@ -935,8 +935,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command method_setup} @{syntax target}?
-      @{syntax name} '=' @{syntax text} @{syntax text}?
+    @@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
   \<close>}
 
   \begin{description}
diff -r 5d801eff5647 -r 00b62aa9f430 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Mar 23 15:54:41 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Mar 23 15:55:41 2015 +0100
@@ -160,20 +160,24 @@
   (global) "end"} has a different meaning: it concludes the theory
   itself (\secref{sec:begin-thy}).
   
-  \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
-  local theory command specifies an immediate target, e.g.\
-  ``@{command "definition"}~@{text "(\<IN> c) \<dots>"}'' or ``@{command
-  "theorem"}~@{text "(\<IN> c) \<dots>"}''.  This works both in a local or
-  global theory context; the current target context will be suspended
-  for this command only.  Note that ``@{text "(\<IN> -)"}'' will
-  always produce a global result independently of the current target
-  context.
+  \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
+  theory command specifies an immediate target, e.g.\ ``@{command
+  "definition"}~@{text "(\<IN> c)"}'' or ``@{command "theorem"}~@{text
+  "(\<IN> c)"}''. This works both in a local or global theory context; the
+  current target context will be suspended for this command only. Note that
+  ``@{text "(\<IN> -)"}'' will always produce a global result independently
+  of the current target context.
 
   \end{description}
 
-  The exact meaning of results produced within a local theory context
-  depends on the underlying target infrastructure (locale, type class
-  etc.).  The general idea is as follows, considering a context named
+  Any specification element that operates on @{text local_theory} according
+  to this manual implicitly allows the above target syntax @{text
+  "("}@{keyword "in"}~@{text "c)"}, but individual syntax diagrams omit that
+  aspect for clarity.
+
+  \medskip The exact meaning of results produced within a local theory
+  context depends on the underlying target infrastructure (locale, type
+  class etc.). The general idea is as follows, considering a context named
   @{text c} with parameter @{text x} and assumption @{text "A[x]"}.
   
   Definitions are exported by introducing a global version with
@@ -188,11 +192,7 @@
   generalizing the parameters of the context.  For example, @{text "a:
   B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
   @{text "?x"}.
-
-  \medskip The Isabelle/HOL library contains numerous applications of
-  locales and classes, e.g.\ see @{file "~~/src/HOL/Algebra"}.  An
-  example for an unnamed auxiliary contexts is given in @{file
-  "~~/src/HOL/Isar_Examples/Group_Context.thy"}.\<close>
+\<close>
 
 
 section \<open>Bundled declarations \label{sec:bundle}\<close>
@@ -221,8 +221,8 @@
   locale interpretation (\secref{sec:locale}).
 
   @{rail \<open>
-    @@{command bundle} @{syntax target}? \<newline>
-    @{syntax name} '=' @{syntax thmrefs} (@'for' (@{syntax vars} + @'and'))?
+    @@{command bundle} @{syntax name} '=' @{syntax thmrefs}
+      (@'for' (@{syntax vars} + @'and'))?
     ;
     (@@{command include} | @@{command including}) (@{syntax nameref}+)
     ;
@@ -284,10 +284,9 @@
   ``abbreviation''.
 
   @{rail \<open>
-    @@{command definition} @{syntax target}? \<newline>
-      (decl @'where')? @{syntax thmdecl}? @{syntax prop}
+    @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
     ;
-    @@{command abbreviation} @{syntax target}? @{syntax mode}? \<newline>
+    @@{command abbreviation} @{syntax mode}? \<newline>
       (decl @'where')? @{syntax prop}
     ;
 
@@ -399,9 +398,9 @@
 
   @{rail \<open>
     (@@{command declaration} | @@{command syntax_declaration})
-      ('(' @'pervasive' ')')? \<newline> @{syntax target}? @{syntax text}
+      ('(' @'pervasive' ')')? \<newline> @{syntax text}
     ;
-    @@{command declare} @{syntax target}? (@{syntax thmrefs} + @'and')
+    @@{command declare} (@{syntax thmrefs} + @'and')
   \<close>}
 
   \begin{description}
@@ -923,7 +922,7 @@
     @@{command instance} (() | (@{syntax nameref} + @'and') '::' @{syntax arity} |
       @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
     ;
-    @@{command subclass} @{syntax target}? @{syntax nameref}
+    @@{command subclass} @{syntax nameref}
     ;
     @@{command class_deps} ( ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) ) \<newline>
       ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) )? )?
@@ -1143,8 +1142,7 @@
     (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
       @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
     ;
-    @@{command attribute_setup} @{syntax target}?
-      @{syntax name} '=' @{syntax text} @{syntax text}?
+    @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
   \<close>}
 
   \begin{description}
@@ -1408,11 +1406,10 @@
   \end{matharray}
 
   @{rail \<open>
-    (@@{command lemmas} | @@{command theorems}) @{syntax target}? \<newline>
-      (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+    (@@{command lemmas} | @@{command theorems}) (@{syntax thmdef}? @{syntax thmrefs} + @'and') \<newline>
       (@'for' (@{syntax vars} + @'and'))?
     ;
-    @@{command named_theorems} @{syntax target}?
+    @@{command named_theorems}
       (@{syntax name} @{syntax text}? + @'and')
   \<close>}