diff -r c20946f5b6fb -r e9c777bfd78c src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Sat Jun 11 13:57:59 2016 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Sat Jun 11 16:41:11 2016 +0200 @@ -354,7 +354,7 @@ \end{matharray} @{rail \ - @@{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') |