1.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Fri May 16 21:41:07 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Fri May 16 21:53:27 2008 +0200
     1.3 @@ -336,8 +336,7 @@
     1.4  
     1.5    Any goal statement causes some term abbreviations (such as
     1.6    @{variable_ref "?thesis"}) to be bound automatically, see also
     1.7 -  \secref{sec:term-abbrev}.  Furthermore, the local context of a
     1.8 -  (non-atomic) goal is provided via the @{case_ref rule_context} case.
     1.9 +  \secref{sec:term-abbrev}.
    1.10  
    1.11    The optional case names of @{element_ref "obtains"} have a twofold
    1.12    meaning: (1) during the of this claim they refer to the the local