--- a/src/Doc/Isar_Ref/Proof.thy Thu Oct 07 23:42:10 2021 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Fri Oct 08 10:57:05 2021 +0200
@@ -391,9 +391,8 @@
available as @{fact_ref assms} in the proof. Moreover, there are two kinds
of conclusions: @{element_def "shows"} states several simultaneous
propositions (essentially a big conjunction), while @{element_def "obtains"}
- claims several simultaneous simultaneous contexts of (essentially a big
- disjunction of eliminated parameters and assumptions, cf.\
- \secref{sec:obtain}).
+ claims several simultaneous contexts --- essentially a big disjunction of
+ eliminated parameters and assumptions (see \secref{sec:obtain}).
\<^rail>\<open>
(@@{command lemma} | @@{command theorem} | @@{command corollary} |