src/Doc/Isar_Ref/Spec.thy

     ;
     @@{command print_abbrevs} ('!'?)
     ;
     decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'
     ;
-    definition: @{syntax thmdecl}? @{syntax prop} prems @{syntax for_fixes}
-    ;
-    prems: (@'if' ((@{syntax prop}+) + @'and'))?
+    definition: @{syntax thmdecl}? @{syntax prop}
+      @{syntax spec_prems} @{syntax for_fixes}
     ;
     abbreviation: @{syntax prop} @{syntax for_fixes}
   \<close>}
 
   \<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<open>c \<equiv> t\<close> according

 
   @{rail \<open>
     @@{command axiomatization} @{syntax "fixes"}? (@'where' axiomatization)?
     ;
     axiomatization: (@{syntax thmdecl} @{syntax prop} + @'and')
-      prems @{syntax for_fixes}
-    ;
-    prems: (@'if' ((@{syntax prop}+) + @'and'))?
+      @{syntax spec_prems} @{syntax for_fixes}
   \<close>}
 
   \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants
   simultaneously and states axiomatic properties for these. The constants are
   marked as being specified once and for all, which prevents additional