# HG changeset patch
# User wenzelm
# Date 1427126863 -3600
# Node ID 0c73c5eb45f7cd3b036a3af5a3220c56d5322445
# Parent  4e6ab5831cc0430f8a61fc5d48319b9aa8a60940
tuned;

diff -r 4e6ab5831cc0 -r 0c73c5eb45f7 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Mon Mar 23 17:01:47 2015 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Mon Mar 23 17:07:43 2015 +0100
@@ -432,7 +432,7 @@
   @{rail \<open>
     (@@{command lemma} | @@{command theorem} | @@{command corollary} |
      @@{command schematic_lemma} | @@{command schematic_theorem} |
-     @@{command schematic_corollary}) (goal | longgoal)
+     @@{command schematic_corollary}) (goal | statement)
     ;
     (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal
     ;
@@ -441,7 +441,8 @@
   
     goal: (@{syntax props} + @'and')
     ;
-    longgoal: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} * ) conclusion
+    statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
+      conclusion
     ;
     conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
     ;