# HG changeset patch
# User wenzelm
# Date 1427126507 -3600
# Node ID 4e6ab5831cc0430f8a61fc5d48319b9aa8a60940
# Parent  bc04a20e5a378f58038d82fcaa700870baa8bb4d
clarified syntax category "fixes";

diff -r bc04a20e5a37 -r 4e6ab5831cc0 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Mon Mar 23 16:10:32 2015 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Mar 23 17:01:47 2015 +0100
@@ -303,21 +303,17 @@
       @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
     ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
     ;
-    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop}
-    (@'for' (@{syntax vars} + @'and'))?
+    dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') @{syntax for_fixes}
     ;
-    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
-    (@'for' (@{syntax vars} + @'and'))?
+    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
+    ;
+    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
     ;
     @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
     ;
     @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
     ;
     (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
-    ;
-
-    dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
-    (@'for' (@{syntax vars} + @'and'))?
   \<close>}
 
 \begin{description}
diff -r bc04a20e5a37 -r 4e6ab5831cc0 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Mar 23 16:10:32 2015 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Mar 23 17:01:47 2015 +0100
@@ -99,9 +99,9 @@
 
   @{rail \<open>
     (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
-      @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set}) \<newline>
-    @{syntax "fixes"} (@'for' @{syntax "fixes"})? (@'where' clauses)? \<newline>
-    (@'monos' @{syntax thmrefs})?
+      @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
+      @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
+      (@'where' clauses)? (@'monos' @{syntax thmrefs})?
     ;
     clauses: (@{syntax thmdecl}? @{syntax prop} + '|')
     ;
@@ -321,7 +321,7 @@
   command can then be used to establish that the function is total.
 
   \item @{command (HOL) "fun"} is a shorthand notation for ``@{command
-  (HOL) "function"}~@{text "(sequential)"}, followed by automated
+  (HOL) "function"}~@{text "(sequential)"}'', followed by automated
   proof attempts regarding pattern matching and termination.  See
   @{cite "isabelle-function"} for further details.
 
diff -r bc04a20e5a37 -r 4e6ab5831cc0 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Mar 23 16:10:32 2015 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Mar 23 17:01:47 2015 +0100
@@ -352,7 +352,20 @@
   another level of iteration, with explicit @{keyword_ref "and"}
   separators; e.g.\ see @{command "fix"} and @{command "assume"} in
   \secref{sec:proof-context}.
-\<close>
+
+  @{rail \<open>
+    @{syntax_def "fixes"}:
+      ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and')
+    ;
+    @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})?
+  \<close>}
+
+  The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it
+  admits specification of mixfix syntax for the entities that are introduced
+  into the context. An optional suffix ``@{keyword "for"}~@{text "fixes"}''
+  is admitted in many situations to indicate a so-called ``eigen-context''
+  of a formal element: the result will be exported and thus generalized over
+  the given variables.\<close>
 
 
 subsection \<open>Attributes and theorems \label{sec:syn-att}\<close>
diff -r bc04a20e5a37 -r 4e6ab5831cc0 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Mon Mar 23 16:10:32 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Mon Mar 23 17:01:47 2015 +0100
@@ -184,7 +184,7 @@
   \<phi>[t]"}.
 
   @{rail \<open>
-    @@{command fix} (@{syntax vars} + @'and')
+    @@{command fix} @{syntax "fixes"}
     ;
     (@@{command assume} | @@{command presume}) (@{syntax props} + @'and')
     ;
@@ -737,13 +737,11 @@
     ;
     @@{attribute OF} @{syntax thmrefs}
     ;
-    @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? \<newline>
-      (@'for' (@{syntax vars} + @'and'))?
+    @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes}
     ;
     @@{attribute "where"}
       ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
-      (@{syntax type} | @{syntax term}) * @'and') \<newline>
-      (@'for' (@{syntax vars} + @'and'))?
+      (@{syntax type} | @{syntax term}) * @'and') \<newline> @{syntax for_fixes}
   \<close>}
 
   \begin{description}
diff -r bc04a20e5a37 -r 4e6ab5831cc0 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Mar 23 16:10:32 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Mar 23 17:01:47 2015 +0100
@@ -221,8 +221,7 @@
   locale interpretation (\secref{sec:locale}).
 
   @{rail \<open>
-    @@{command bundle} @{syntax name} '=' @{syntax thmrefs}
-      (@'for' (@{syntax vars} + @'and'))?
+    @@{command bundle} @{syntax name} '=' @{syntax thmrefs} @{syntax for_fixes}
     ;
     (@@{command include} | @@{command including}) (@{syntax nameref}+)
     ;
@@ -346,10 +345,6 @@
   @{rail \<open>
     @@{command axiomatization} @{syntax "fixes"}? (@'where' specs)?
     ;
-
-    @{syntax_def "fixes"}: ((@{syntax name} ('::' @{syntax type})?
-      @{syntax mixfix}? | @{syntax vars}) + @'and')
-    ;
     specs: (@{syntax thmdecl}? @{syntax props} + @'and')
   \<close>}
 
@@ -464,7 +459,7 @@
   omitted according to roundup.
 
   @{rail \<open>
-    @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax "fixes"} + @'and'))?
+    @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
     ;
     instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
     ;
@@ -524,7 +519,7 @@
       @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
     ;
     @{syntax_def context_elem}:
-      @'fixes' (@{syntax "fixes"} + @'and') |
+      @'fixes' @{syntax "fixes"} |
       @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
       @'assumes' (@{syntax props} + @'and') |
       @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |
@@ -1406,11 +1401,10 @@
   \end{matharray}
 
   @{rail \<open>
-    (@@{command lemmas} | @@{command theorems}) (@{syntax thmdef}? @{syntax thmrefs} + @'and') \<newline>
-      (@'for' (@{syntax vars} + @'and'))?
+    (@@{command lemmas} | @@{command theorems}) (@{syntax thmdef}? @{syntax thmrefs} + @'and')
+      @{syntax for_fixes}
     ;
-    @@{command named_theorems}
-      (@{syntax name} @{syntax text}? + @'and')
+    @@{command named_theorems} (@{syntax name} @{syntax text}? + @'and')
   \<close>}
 
   \begin{description}