--- 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
--- 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)} \\