--- a/doc-src/IsarRef/Thy/document/Proof.tex Sun May 18 17:03:26 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Sun May 18 17:04:48 2008 +0200
@@ -343,8 +343,7 @@
Any goal statement causes some term abbreviations (such as
\indexref{}{variable}{?thesis}\hyperlink{variable.?thesis}{\mbox{\isa{{\isacharquery}thesis}}}) to be bound automatically, see also
- \secref{sec:term-abbrev}. Furthermore, the local context of a
- (non-atomic) goal is provided via the \indexref{}{case}{rule\_context}\hyperlink{case.rule-context}{\mbox{\isa{rule{\isacharunderscore}context}}} case.
+ \secref{sec:term-abbrev}.
The optional case names of \indexref{}{element}{obtains}\hyperlink{element.obtains}{\mbox{\isa{\isakeyword{obtains}}}} have a twofold
meaning: (1) during the of this claim they refer to the the local