src/Doc/Isar_Ref/Proof.thy
changeset 57979 fc136831d6ca
parent 57947 189d421ca72d
parent 57973 decf2e9289ab
child 58552 66fed99e874f
     1.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sun Aug 17 22:27:58 2014 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Mon Aug 18 13:19:04 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