# HG changeset patch
# User wenzelm
# Date 1429382695 -7200
# Node ID 8044de95819b1beb096727988c22737403a29c98
# Parent  3d696ccb7fa6f816136e55675d1eef541618ccaf
clarified syntax diagram: 'obtains' does not allow prop_pat (although it could and should at some point);

diff -r 3d696ccb7fa6 -r 8044de95819b src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Fri Apr 17 19:49:40 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat Apr 18 20:44:55 2015 +0200
@@ -444,9 +444,9 @@
     statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
       conclusion
     ;
-    conclusion: @'shows' goal | @'obtains' (@{syntax parname}? case + '|')
+    conclusion: @'shows' goal | @'obtains' (@{syntax parname}? obtain_case + '|')
     ;
-    case: (@{syntax vars} + @'and') @'where' (@{syntax props} + @'and')
+    obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
   \<close>}
 
   \begin{description}