# HG changeset patch
# User wenzelm
# Date 1211123088 -7200
# Node ID 290e1571c82946ff1ea6798985396abfc55824e0
# Parent  1aa5cd390dfbb92bf07b4990111d5a80f9062632
updated generated file;

diff -r 1aa5cd390dfb -r 290e1571c829 doc-src/IsarImplementation/Thy/document/base.tex
--- a/doc-src/IsarImplementation/Thy/document/base.tex	Sun May 18 17:03:26 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/base.tex	Sun May 18 17:04:48 2008 +0200
@@ -12,7 +12,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ base\isanewline
-\isakeyword{imports}\ CPure\isanewline
+\isakeyword{imports}\ Pure\isanewline
 \isakeyword{uses}\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isacharslash}{\isachardot}{\isachardot}{\isacharslash}antiquote{\isacharunderscore}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
 \isakeyword{begin}\isanewline
 \isanewline
diff -r 1aa5cd390dfb -r 290e1571c829 doc-src/IsarRef/Thy/document/Proof.tex
--- 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
diff -r 1aa5cd390dfb -r 290e1571c829 doc-src/IsarRef/Thy/document/intro.tex
--- a/doc-src/IsarRef/Thy/document/intro.tex	Sun May 18 17:03:26 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/intro.tex	Sun May 18 17:04:48 2008 +0200
@@ -11,7 +11,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ intro\isanewline
-\isakeyword{imports}\ CPure\isanewline
+\isakeyword{imports}\ Pure\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
diff -r 1aa5cd390dfb -r 290e1571c829 doc-src/IsarRef/Thy/document/pure.tex
--- a/doc-src/IsarRef/Thy/document/pure.tex	Sun May 18 17:03:26 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/pure.tex	Sun May 18 17:04:48 2008 +0200
@@ -11,7 +11,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ pure\isanewline
-\isakeyword{imports}\ CPure\isanewline
+\isakeyword{imports}\ Pure\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
diff -r 1aa5cd390dfb -r 290e1571c829 doc-src/IsarRef/Thy/document/syntax.tex
--- a/doc-src/IsarRef/Thy/document/syntax.tex	Sun May 18 17:03:26 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/syntax.tex	Sun May 18 17:04:48 2008 +0200
@@ -11,7 +11,7 @@
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
 \ {\isachardoublequoteopen}syntax{\isachardoublequoteclose}\isanewline
-\isakeyword{imports}\ CPure\isanewline
+\isakeyword{imports}\ Pure\isanewline
 \isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%