# HG changeset patch
# User wenzelm
# Date 1212444232 -7200
# Node ID d58b0fd31b592c27b25e9a0ec452d5325dde00ce
# Parent  5c48cecb981b663cd3d0d0a443e0e3fbd276e5b9
tuned;

diff -r 5c48cecb981b -r d58b0fd31b59 doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Mon Jun 02 23:38:28 2008 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Tue Jun 03 00:03:52 2008 +0200
@@ -90,11 +90,12 @@
   markup just preceding the formal beginning of a theory.  In actual
   document preparation the corresponding {\LaTeX} macro @{verbatim
   "\\isamarkupheader"} may be redefined to produce chapter or section
-  headings.  See also \secref{sec:markup} for further markup commands.
+  headings.
   
   \item [@{command "chapter"}, @{command "section"}, @{command
   "subsection"}, and @{command "subsubsection"}] mark chapter and
-  section headings.
+  section headings.  The corresponding {\LaTeX} macros are @{verbatim
+  "\\isamarkupchapter"}, @{verbatim "\\isamarkupsection"} etc.
 
   \item [@{command "text"} and @{command "txt"}] specify paragraphs of
   plain text.
@@ -155,8 +156,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 ``@{text "@{term [show_types] \"f x = a + x\"}"}''
   within a text block would cause
diff -r 5c48cecb981b -r d58b0fd31b59 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Mon Jun 02 23:38:28 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Tue Jun 03 00:03:52 2008 +0200
@@ -710,15 +710,9 @@
 *}
 
 
-section {* Axiomatic type classes \label{sec:axclass} *}
+subsection {* Old-style axiomatic type classes \label{sec:axclass} *}
 
 text {*
-  \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}
     @{command_def "axclass"} & : & \isartrans{theory}{theory} \\
     @{command_def "instance"} & : & \isartrans{theory}{proof(prove)} \\