# HG changeset patch
# User wenzelm
# Date 1234813779 -3600
# Node ID df70c029157950ce82a370f1f360ef4ca584d701
# Parent  d66b34e46bdf07655e7008eba17b3a36951e4ae3
updated generated files;

diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/Base.tex
--- a/doc-src/IsarImplementation/Thy/document/Base.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Base.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -1,17 +1,14 @@
 %
 \begin{isabellebody}%
-\def\isabellecontext{base}%
+\def\isabellecontext{Base}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ base\isanewline
+\ Base\isanewline
 \isakeyword{imports}\ Pure\isanewline
 \isakeyword{uses}\ {\isachardoublequoteopen}{\isachardot}{\isachardot}{\isacharslash}{\isachardot}{\isachardot}{\isacharslash}antiquote{\isacharunderscore}setup{\isachardot}ML{\isachardoublequoteclose}\isanewline
 \isakeyword{begin}\isanewline
diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/Integration.tex
--- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -1,17 +1,16 @@
 %
 \begin{isabellebody}%
-\def\isabellecontext{integration}%
+\def\isabellecontext{Integration}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ integration\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\ Integration\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %
diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/Isar.tex
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -1,17 +1,16 @@
 %
 \begin{isabellebody}%
-\def\isabellecontext{isar}%
+\def\isabellecontext{Isar}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ isar\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\ Isar\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %
diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/Local_Theory.tex
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -1,17 +1,16 @@
 %
 \begin{isabellebody}%
-\def\isabellecontext{locale}%
+\def\isabellecontext{Local{\isacharunderscore}Theory}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ {\isachardoublequoteopen}locale{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\ Local{\isacharunderscore}Theory\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %
diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -1,6 +1,6 @@
 %
 \begin{isabellebody}%
-\def\isabellecontext{logic}%
+\def\isabellecontext{Logic}%
 %
 \isadelimtheory
 %
@@ -8,7 +8,9 @@
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ logic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\ Logic\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %
diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -3,14 +3,14 @@
 \def\isabellecontext{ML}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %
diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -1,17 +1,16 @@
 %
 \begin{isabellebody}%
-\def\isabellecontext{prelim}%
+\def\isabellecontext{Prelim}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ prelim\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\ Prelim\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %
diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/Proof.tex
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -1,17 +1,16 @@
 %
 \begin{isabellebody}%
-\def\isabellecontext{proof}%
+\def\isabellecontext{Proof}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ {\isachardoublequoteopen}proof{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\ Proof\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %
diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/Tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -1,17 +1,16 @@
 %
 \begin{isabellebody}%
-\def\isabellecontext{tactic}%
+\def\isabellecontext{Tactic}%
 %
 \isadelimtheory
-\isanewline
-\isanewline
-\isanewline
 %
 \endisadelimtheory
 %
 \isatagtheory
 \isacommand{theory}\isamarkupfalse%
-\ tactic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\ Tactic\isanewline
+\isakeyword{imports}\ Base\isanewline
+\isakeyword{begin}%
 \endisatagtheory
 {\isafoldtheory}%
 %
@@ -504,7 +503,6 @@
 %
 \endisadelimtheory
 \isanewline
-\isanewline
 \end{isabellebody}%
 %%% Local Variables:
 %%% mode: latex
diff -r d66b34e46bdf -r df70c0291579 doc-src/IsarImplementation/Thy/document/session.tex
--- a/doc-src/IsarImplementation/Thy/document/session.tex	Mon Feb 16 20:47:44 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/session.tex	Mon Feb 16 20:49:39 2009 +0100
@@ -1,18 +1,18 @@
-\input{base.tex}
+\input{Base.tex}
 
-\input{prelim.tex}
+\input{Prelim.tex}
 
-\input{logic.tex}
+\input{Logic.tex}
 
-\input{tactic.tex}
+\input{Tactic.tex}
 
-\input{proof.tex}
+\input{Proof.tex}
 
-\input{isar.tex}
+\input{Isar.tex}
 
-\input{locale.tex}
+\input{Local_Theory.tex}
 
-\input{integration.tex}
+\input{Integration.tex}
 
 \input{ML.tex}