# HG changeset patch
# User wenzelm
# Date 1212444234 -7200
# Node ID f1ef0973d0a811cb4f19642b1fad691091ee9d1e
# Parent  d58b0fd31b592c27b25e9a0ec452d5325dde00ce
updated generated file;

diff -r d58b0fd31b59 -r f1ef0973d0a8 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue Jun 03 00:03:52 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue Jun 03 00:03:54 2008 +0200
@@ -109,10 +109,10 @@
   \item [\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
   markup just preceding the formal beginning of a theory.  In actual
   document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
-  headings.  See also \secref{sec:markup} for further markup commands.
+  headings.
   
   \item [\hyperlink{command.chapter}{\mbox{\isa{\isacommand{chapter}}}}, \hyperlink{command.section}{\mbox{\isa{\isacommand{section}}}}, \hyperlink{command.subsection}{\mbox{\isa{\isacommand{subsection}}}}, and \hyperlink{command.subsubsection}{\mbox{\isa{\isacommand{subsubsection}}}}] mark chapter and
-  section headings.
+  section headings.  The corresponding {\LaTeX} macros are \verb|\isamarkupchapter|, \verb|\isamarkupsection| etc.
 
   \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} and \hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}] specify paragraphs of
   plain text.
@@ -172,8 +172,7 @@
   The text body of formal comments (see also \secref{sec:comments})
   may contain antiquotations of logical entities, such as theorems,
   terms and types, which are to be presented in the final output
-  produced by the Isabelle document preparation system (see also
-  \chref{ch:document-prep}).
+  produced by the Isabelle document preparation system.
 
   Thus embedding of ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
   within a text block would cause
diff -r d58b0fd31b59 -r f1ef0973d0a8 doc-src/IsarRef/Thy/document/Misc.tex
--- a/doc-src/IsarRef/Thy/document/Misc.tex	Tue Jun 03 00:03:52 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Misc.tex	Tue Jun 03 00:03:54 2008 +0200
@@ -235,7 +235,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{System operations%
+\isamarkupsection{System commands%
 }
 \isamarkuptrue%
 %
diff -r d58b0fd31b59 -r f1ef0973d0a8 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Tue Jun 03 00:03:52 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue Jun 03 00:03:54 2008 +0200
@@ -713,18 +713,12 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Axiomatic type classes \label{sec:axclass}%
+\isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-\begin{warn}
-  This describes the old interface to axiomatic type-classes in
-  Isabelle.  See \secref{sec:class} for a more recent higher-level
-  view on the same ideas.
-  \end{warn}
-
-  \begin{matharray}{rcl}
+\begin{matharray}{rcl}
     \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\
     \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{theory}{proof(prove)} \\
   \end{matharray}