# HG changeset patch
# User wenzelm
# Date 1407953309 -7200
# Node ID decf2e9289ab7a6f489b0c7a79c46b0b35eb2ab4
# Parent  3381502bf264015f35ec00c3a7243b1144010636
tuned;

diff -r 3381502bf264 -r decf2e9289ab src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Aug 13 15:45:41 2014 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Aug 13 20:08:29 2014 +0200
@@ -520,10 +520,10 @@
   \secref{sec:term-abbrev}.
 
   The optional case names of @{element_ref "obtains"} have a twofold
-  meaning: (1) during the of this claim they refer to the the local
-  context introductions, (2) the resulting rule is annotated
-  accordingly to support symbolic case splits when used with the
-  @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
+  meaning: (1) in the proof of this claim they refer to the local context
+  introductions, (2) in the resulting rule they become annotations for
+  symbolic case splits, e.g.\ for the @{method_ref cases} method
+  (\secref{sec:cases-induct}).
 *}