merged

--- a/NEWS	Sat Jun 11 17:23:24 2016 +0200
+++ b/NEWS	Sat Jun 11 17:40:52 2016 +0200
@@ -93,7 +93,7 @@
 'definition', 'inductive', 'function'.
 
 * Toplevel theorem statements support eigen-context notation with 'if' /
-'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
+'for' (in postfix), which corresponds to 'assumes' / 'fixes' in the
 traditional long statement form (in prefix). Local premises are called
 "that" or "assms", respectively. Empty premises are *not* bound in the
 context: INCOMPATIBILITY.

--- a/lib/texinputs/isabellesym.sty	Sat Jun 11 17:23:24 2016 +0200
+++ b/lib/texinputs/isabellesym.sty	Sat Jun 11 17:40:52 2016 +0200
@@ -359,11 +359,11 @@
 \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
 \newcommand{\isasymmodule}{\isamath{\langle}\isakeyword{module}\isamath{\rangle}}
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
 \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
 \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
-\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
-\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
 \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
 \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
+\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
 \newcommand{\isasymcomment}{\isatext{---}}
 \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Jun 11 17:40:52 2016 +0200
@@ -108,7 +108,7 @@
   @{rail \<open>
     (@@{command (HOL) inductive} | @@{command (HOL) inductive_set} |
       @@{command (HOL) coinductive} | @@{command (HOL) coinductive_set})
-      @{syntax "fixes"} @{syntax "for_fixes"} \<newline>
+      @{syntax vars} @{syntax for_fixes} \<newline>
       (@'where' @{syntax multi_specs})? (@'monos' @{syntax thms})?
     ;
     @@{command print_inductives} ('!'?)

--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Sat Jun 11 17:40:52 2016 +0200
@@ -346,7 +346,9 @@
   to introduce multiple such items simultaneously.
 
   @{rail \<open>
-    @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
+    @{syntax_def vars}:
+      (((@{syntax name} +) ('::' @{syntax type})? |
+        @{syntax name} ('::' @{syntax type})? @{syntax mixfix}) + @'and')
     ;
     @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
     ;
@@ -361,20 +363,6 @@
   another level of iteration, with explicit @{keyword_ref "and"} separators;
   e.g.\ see @{command "fix"} and @{command "assume"} in
   \secref{sec:proof-context}.
-
-  @{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"}~\<open>fixes\<close>'' 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>
 
 
@@ -463,6 +451,8 @@
 
 
   @{rail \<open>
+    @{syntax_def for_fixes}: (@'for' @{syntax vars})?
+    ;
     @{syntax_def multi_specs}: (@{syntax structured_spec} + '|')
     ;
     @{syntax_def structured_spec}:
@@ -470,7 +460,7 @@
     ;
     @{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))?
     ;
-    @{syntax_def specification}: @{syntax "fixes"} @'where' @{syntax multi_specs}
+    @{syntax_def specification}: @{syntax vars} @'where' @{syntax multi_specs}
   \<close>}
 \<close>
 

--- a/src/Doc/Isar_Ref/Proof.thy	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat Jun 11 17:40:52 2016 +0200
@@ -159,7 +159,7 @@
   \<phi>[t]\<close>.
 
   @{rail \<open>
-    @@{command fix} @{syntax "fixes"}
+    @@{command fix} @{syntax vars}
     ;
     (@@{command assume} | @@{command presume}) concl prems @{syntax for_fixes}
     ;
@@ -167,8 +167,8 @@
     ;
     prems: (@'if' (@{syntax props'} + @'and'))?
     ;
-    @@{command define} (@{syntax "fixes"} + @'and')
-      @'where' (@{syntax props} + @'and') @{syntax for_fixes}
+    @@{command define} @{syntax vars} @'where'
+      (@{syntax props} + @'and') @{syntax for_fixes}
     ;
     @@{command def} (def + @'and')
     ;
@@ -417,7 +417,7 @@
     ;
     @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')
     ;
-    @{syntax_def obtain_case}: (@{syntax vars} + @'and') @'where'
+    @{syntax_def obtain_case}: @{syntax vars} @'where'
       (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>}
 
@@ -1335,14 +1335,14 @@
   @{rail \<open>
     @@{command consider} @{syntax obtain_clauses}
     ;
-    @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') \<newline>
+    @@{command obtain} @{syntax par_name}? @{syntax vars} \<newline>
       @'where' concl prems @{syntax for_fixes}
     ;
     concl: (@{syntax props} + @'and')
     ;
     prems: (@'if' (@{syntax props'} + @'and'))?
     ;
-    @@{command guess} (@{syntax "fixes"} + @'and')
+    @@{command guess} @{syntax vars}
   \<close>}
 
   \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)

--- a/src/Doc/Isar_Ref/Quick_Reference.thy	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Quick_Reference.thy	Sat Jun 11 17:40:52 2016 +0200
@@ -13,17 +13,20 @@
 text \<open>
   \begin{tabular}{rcl}
     \<open>main\<close> & = & \<^theory_text>\<open>notepad begin "statement\<^sup>*" end\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>theorem name: props "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>theorem name: props if props for vars "proof"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
-    & & \quad\<^theory_text>\<open>fixes "var\<^sup>+"\<close> \\
+    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
     & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
     & & \quad\<^theory_text>\<open>shows name: props "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>theorem name:\<close> \\
+    & & \quad\<^theory_text>\<open>fixes vars\<close> \\
+    & & \quad\<^theory_text>\<open>assumes name: props\<close> \\
+    & & \quad\<^theory_text>\<open>obtains (name) vars where props | \<dots> "proof"\<close> \\
     \<open>proof\<close> & = & \<^theory_text>\<open>"refinement\<^sup>*" proof "method\<^sup>?" "statement\<^sup>*" qed "method\<^sup>?"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>"refinement\<^sup>*" done\<close> \\
     \<open>refinement\<close> & = &  \<^theory_text>\<open>apply method\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>supply facts\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>subgoal "proof"\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>subgoal for "var\<^sup>+" "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>subgoal premises name for vars "proof"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>using facts\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>unfolding facts\<close> \\
     \<open>statement\<close> & = & \<^theory_text>\<open>{ "statement\<^sup>*" }\<close> \\
@@ -31,14 +34,11 @@
     & \<open>|\<close> & \<^theory_text>\<open>note name = facts\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>let "term" = "term"\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>write name  (mixfix)\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>fix "var\<^sup>+"\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>assume name: props\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for "var\<^sup>+"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>fix vars\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>assume name: props if props for vars\<close> \\
     & \<open>|\<close> & \<^theory_text>\<open>then"\<^sup>?" goal\<close> \\
-    \<open>goal\<close> & = & \<^theory_text>\<open>have name: props "proof"\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>have name: props if name: props for "var\<^sup>+" "proof"\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>show name: props "proof"\<close> \\
-    & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for "var\<^sup>+" "proof"\<close> \\
+    \<open>goal\<close> & = & \<^theory_text>\<open>have name: props if name: props for vars "proof"\<close> \\
+    & \<open>|\<close> & \<^theory_text>\<open>show name: props if name: props for vars "proof"\<close> \\
   \end{tabular}
 \<close>
 

--- a/src/Doc/Isar_Ref/Spec.thy	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Jun 11 17:40:52 2016 +0200
@@ -354,7 +354,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
+    @@{command axiomatization} @{syntax vars}? (@'where' axiomatization)?
     ;
     axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
       @{syntax spec_prems} @{syntax for_fixes}
@@ -516,7 +516,7 @@
       @{syntax locale_expr} ('+' (@{syntax context_elem}+))?
     ;
     @{syntax_def context_elem}:
-      @'fixes' @{syntax "fixes"} |
+      @'fixes' @{syntax vars} |
       @'constrains' (@{syntax name} '::' @{syntax type} + @'and') |
       @'assumes' (@{syntax props} + @'and') |
       @'defines' (@{syntax thmdecl}? @{syntax prop} @{syntax prop_pat}? + @'and') |

--- a/src/HOL/HOLCF/Tools/fixrec.ML	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Jun 11 17:40:52 2016 +0200
@@ -400,7 +400,7 @@
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword fixrec} "define recursive functions (HOLCF)"
-    (Parse.fixes -- (Parse.where_ |-- Parse.!!! multi_specs')
-      >> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
+    (Parse.vars -- (Parse.where_ |-- Parse.!!! multi_specs')
+      >> (fn (vars, specs) => add_fixrec_cmd vars specs))
 
 end

--- a/src/HOL/Library/rewrite.ML	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/HOL/Library/rewrite.ML	Sat Jun 11 17:40:52 2016 +0200
@@ -333,7 +333,7 @@
         val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
         val atom =  (Args.$$$ "asm" >> K Asm) ||
           (Args.$$$ "concl" >> K Concl) ||
-          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.fixes []) >> For) ||
+          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.vars []) >> For) ||
           (Parse.term >> Term)
         val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
 

--- a/src/HOL/Nominal/nominal_primrec.ML	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Jun 11 17:40:52 2016 +0200
@@ -403,8 +403,8 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword nominal_primrec}
     "define primitive recursive functions on nominal datatypes"
-    (options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_multi_specs
-      >> (fn ((((invs, fctxt), fixes), params), specs) =>
-        primrec_cmd invs fctxt fixes params specs));
+    (options -- Parse.vars -- Parse.for_fixes -- Parse_Spec.where_multi_specs
+      >> (fn ((((invs, fctxt), vars), params), specs) =>
+        primrec_cmd invs fctxt vars params specs));
 
 end;

--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Sat Jun 11 17:40:52 2016 +0200
@@ -2394,13 +2394,13 @@
 val _ = Outer_Syntax.local_theory @{command_keyword corec}
   "define nonprimitive corecursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
-      --| @{keyword ")"}) []) -- (Parse.fixes --| Parse.where_ -- Parse.prop)
+      --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
    >> uncurry corec_cmd);
 
 val _ = Outer_Syntax.local_theory_to_proof @{command_keyword corecursive}
   "define nonprimitive corecursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
-      --| @{keyword ")"}) []) -- (Parse.fixes --| Parse.where_ -- Parse.prop)
+      --| @{keyword ")"}) []) -- (Parse.vars --| Parse.where_ -- Parse.prop)
    >> uncurry corecursive_cmd);
 
 val _ = Outer_Syntax.local_theory_to_proof @{command_keyword friend_of_corec}

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Sat Jun 11 17:40:52 2016 +0200
@@ -1615,13 +1615,13 @@
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |--
       Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
-    (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd);
+    (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorecursive_cmd);
 
 val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
   "define primitive corecursive functions"
   ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
       --| @{keyword ")"}) []) --
-    (Parse.fixes -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
+    (Parse.vars -- where_alt_props_of_parser) >> uncurry primcorec_cmd);
 
 val _ = Theory.setup (gfp_rec_sugar_interpretation transfer_plugin
   gfp_rec_sugar_transfer_interpretation);

--- a/src/HOL/Tools/Function/partial_function.ML	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Sat Jun 11 17:40:52 2016 +0200
@@ -313,7 +313,7 @@
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
-    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.simple_spec)))
-      >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
+    ((mode -- (Parse.vars -- (Parse.where_ |-- Parse_Spec.simple_spec)))
+      >> (fn (mode, (vars, spec)) => add_partial_function_cmd mode vars spec));
 
 end;

--- a/src/HOL/Tools/inductive.ML	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Jun 11 17:40:52 2016 +0200
@@ -1169,7 +1169,7 @@
 (** outer syntax **)
 
 fun gen_ind_decl mk_def coind =
-  Parse.fixes -- Parse.for_fixes --
+  Parse.vars -- Parse.for_fixes --
   Scan.optional Parse_Spec.where_multi_specs [] --
   Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.thms1) []
   >> (fn (((preds, params), specs), monos) =>

--- a/src/Pure/Isar/parse.ML	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/Pure/Isar/parse.ML	Sat Jun 11 17:40:52 2016 +0200
@@ -88,7 +88,7 @@
   val const_decl: (string * string * mixfix) parser
   val const_binding: (binding * string * mixfix) parser
   val params: (binding * string option * mixfix) list parser
-  val fixes: (binding * string option * mixfix) list parser
+  val vars: (binding * string option * mixfix) list parser
   val for_fixes: (binding * string option * mixfix) list parser
   val ML_source: Input.source parser
   val document_source: Input.source parser
@@ -374,8 +374,9 @@
     >> (fn ((x, ys), T) =>
         (x, Option.map #1 T, NoSyn) :: map (fn y => (y, Option.map #2 T, NoSyn)) ys);
 
-val fixes = and_list1 (param_mixfix || params) >> flat;
-val for_fixes = Scan.optional ($$$ "for" |-- !!! fixes) [];
+val vars = and_list1 (param_mixfix || params) >> flat;
+
+val for_fixes = Scan.optional ($$$ "for" |-- !!! vars) [];
 
 
 (* embedded source text *)

--- a/src/Pure/Isar/parse_spec.ML	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Sat Jun 11 17:40:52 2016 +0200
@@ -67,7 +67,7 @@
 
 val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs;
 
-val specification = Parse.fixes -- where_multi_specs;
+val specification = Parse.vars -- where_multi_specs;
 
 
 (* basic constant specifications *)
@@ -157,7 +157,7 @@
 
 val obtain_case =
   Parse.parbinding --
-    (Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] --
+    (Scan.optional (Parse.and_list1 Parse.vars --| Parse.where_ >> flat) [] --
       (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
 
 val obtains = Parse.enum1 "|" obtain_case;

--- a/src/Pure/Pure.thy	Sat Jun 11 17:23:24 2016 +0200
+++ b/src/Pure/Pure.thy	Sat Jun 11 17:40:52 2016 +0200
@@ -359,7 +359,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword axiomatization} "axiomatic constant specification"
-    (Scan.optional Parse.fixes [] --
+    (Scan.optional Parse.vars [] --
       Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
       >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
 
@@ -756,7 +756,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword fix} "fix local variables (Skolem constants)"
-    (Parse.fixes >> (Toplevel.proof o Proof.fix_cmd));
+    (Parse.vars >> (Toplevel.proof o Proof.fix_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword assume} "assume propositions"
@@ -768,7 +768,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword define} "local definition (non-polymorphic)"
-    ((Parse.fixes --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
+    ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes
       >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b)));
 
 val _ =
@@ -786,12 +786,12 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword obtain} "generalized elimination"
-    (Parse.parbinding -- Scan.optional (Parse.fixes --| Parse.where_) [] -- structured_statement
+    (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement
       >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e)));
 
 val _ =
   Outer_Syntax.command @{command_keyword guess} "wild guessing (unstructured)"
-    (Scan.optional Parse.fixes [] >> (Toplevel.proof' o Obtain.guess_cmd));
+    (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd));
 
 val _ =
   Outer_Syntax.command @{command_keyword let} "bind text variables"