--- a/src/Doc/Isar_Ref/Proof.thy Sat Apr 18 20:44:55 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Sat Apr 18 20:46:48 2015 +0200
@@ -444,7 +444,7 @@
statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
conclusion
;
- conclusion: @'shows' goal | @'obtains' (@{syntax parname}? obtain_case + '|')
+ conclusion: @'shows' goal | @'obtains' (@{syntax par_name}? obtain_case + '|')
;
obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
\<close>}
@@ -989,7 +989,7 @@
occur in the conclusion.
@{rail \<open>
- @@{command obtain} @{syntax parname}? (@{syntax vars} + @'and')
+ @@{command obtain} @{syntax par_name}? (@{syntax vars} + @'and')
@'where' (@{syntax props} + @'and')
;
@@{command guess} (@{syntax vars} + @'and')