# HG changeset patch
# User wenzelm
# Date 1633683425 -7200
# Node ID e593ea8804946ea119044593ae3dc961161775ca
# Parent  f4c5e8ca1d53304bbb6eab36782a9b7fa7ebfc29
tuned text;

diff -r f4c5e8ca1d53 -r e593ea880494 src/Doc/Isar_Ref/Proof.thy
--- 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} |