diff -r 0824fd1e9c40 -r f25f2f2ba48c src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Jun 10 11:52:54 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Jun 10 14:46:31 2015 +0200
@@ -435,13 +435,15 @@
      @@{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
     ;