--- 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
;