--- 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
--- 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
--- 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}%
--- 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}%
--- 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}%