--- a/src/Doc/Isar_Ref/Proof.thy Thu Jun 11 22:47:53 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Sat Jun 13 13:09:05 2015 +0200
@@ -435,15 +435,13 @@
@@{command schematic_corollary}) (stmt | statement)
;
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
- stmt if_prems @{syntax for_fixes}
+ stmt (@'if' stmt)? @{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
;