src/Doc/Isar_Ref/Proof.thy

     (@@{command lemma} | @@{command theorem} | @@{command corollary} |
      @@{command schematic_lemma} | @@{command schematic_theorem} |
      @@{command schematic_corollary}) (stmt | statement)
     ;
     (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
-      stmt @{syntax for_fixes}
+      stmt if_prems @{syntax for_fixes}
     ;
     @@{command print_statement} @{syntax modes}? @{syntax thmrefs}
     ;
   
     stmt: (@{syntax props} + @'and')
+    ;
+    if_prems: (@'if' stmt)?
     ;
     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
       conclusion
     ;
     conclusion: @'shows' stmt | @'obtains' (@{syntax par_name}? obtain_case + '|')