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