src/Doc/Isar_Ref/Spec.thy

   a certain form (see also \secref{sec:overloading}), or outside of it as
   rewrite system on abstract syntax. The second form is called
   ``abbreviation''.
 
   @{rail \<open>
-    @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
-    ;
-    @@{command abbreviation} @{syntax mode}? \<newline>
-      (decl @'where')? @{syntax prop}
-    ;
-    decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
+    @@{command definition} decl? definition
+    ;
+    @@{command abbreviation} @{syntax mode}? decl? abbreviation
     ;
     @@{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'))?
+    ;
+    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
   to the specification given as \<open>eq\<close>, which is then turned into a proven fact.
   The given proposition may deviate from internal meta-level equality