1.1 --- a/src/Doc/Isar_Ref/Proof.thy	Wed Aug 13 15:45:41 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Wed Aug 13 20:08:29 2014 +0200
     1.3 @@ -520,10 +520,10 @@
     1.4    \secref{sec:term-abbrev}.
     1.5  
     1.6    The optional case names of @{element_ref "obtains"} have a twofold
     1.7 -  meaning: (1) during the of this claim they refer to the the local
     1.8 -  context introductions, (2) the resulting rule is annotated
     1.9 -  accordingly to support symbolic case splits when used with the
    1.10 -  @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
    1.11 +  meaning: (1) in the proof of this claim they refer to the local context
    1.12 +  introductions, (2) in the resulting rule they become annotations for
    1.13 +  symbolic case splits, e.g.\ for the @{method_ref cases} method
    1.14 +  (\secref{sec:cases-induct}).
    1.15  *}
    1.16  
    1.17