--- a/src/Doc/Implementation/Proof.thy Fri Sep 24 22:44:13 2021 +0200
+++ b/src/Doc/Implementation/Proof.thy Sun Sep 26 18:49:55 2021 +0200
@@ -352,10 +352,11 @@
means of a given tactic. This acts like a dual conclusion: the proof
demonstrates that the context may be augmented by parameters and
assumptions, without affecting any conclusions that do not mention these
- parameters. See also @{cite "isabelle-isar-ref"} for the user-level
- @{command obtain} and @{command guess} elements. Final results, which may
- not refer to the parameters in the conclusion, need to exported explicitly
- into the original context.\<close>
+ parameters. See also @{cite "isabelle-isar-ref"} for the corresponding Isar
+ proof command @{command obtain}. Final results, which may not refer to the
+ parameters in the conclusion, need to exported explicitly into the original
+ context.
+\<close>
text %mlref \<open>
\begin{mldecls}