--- 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}
--- 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.
--- 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>
--- 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}
--- 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}