updated generated file;
authorwenzelm
Tue Jun 03 00:03:54 2008 +0200 (2008-06-03)
changeset 27054f1ef0973d0a8
parent 27053 d58b0fd31b59
child 27055 4a99797aa9f2
updated generated file;
doc-src/IsarRef/Thy/document/Document_Preparation.tex
doc-src/IsarRef/Thy/document/Misc.tex
doc-src/IsarRef/Thy/document/Spec.tex
     1.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue Jun 03 00:03:52 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue Jun 03 00:03:54 2008 +0200
     1.3 @@ -109,10 +109,10 @@
     1.4    \item [\hyperlink{command.header}{\mbox{\isa{\isacommand{header}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
     1.5    markup just preceding the formal beginning of a theory.  In actual
     1.6    document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
     1.7 -  headings.  See also \secref{sec:markup} for further markup commands.
     1.8 +  headings.
     1.9    
    1.10    \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
    1.11 -  section headings.
    1.12 +  section headings.  The corresponding {\LaTeX} macros are \verb|\isamarkupchapter|, \verb|\isamarkupsection| etc.
    1.13  
    1.14    \item [\hyperlink{command.text}{\mbox{\isa{\isacommand{text}}}} and \hyperlink{command.txt}{\mbox{\isa{\isacommand{txt}}}}] specify paragraphs of
    1.15    plain text.
    1.16 @@ -172,8 +172,7 @@
    1.17    The text body of formal comments (see also \secref{sec:comments})
    1.18    may contain antiquotations of logical entities, such as theorems,
    1.19    terms and types, which are to be presented in the final output
    1.20 -  produced by the Isabelle document preparation system (see also
    1.21 -  \chref{ch:document-prep}).
    1.22 +  produced by the Isabelle document preparation system.
    1.23  
    1.24    Thus embedding of ``\isa{{\isachardoublequote}{\isacharat}{\isacharbraceleft}term\ {\isacharbrackleft}show{\isacharunderscore}types{\isacharbrackright}\ {\isachardoublequote}f\ x\ {\isacharequal}\ a\ {\isacharplus}\ x{\isachardoublequote}{\isacharbraceright}{\isachardoublequote}}''
    1.25    within a text block would cause
     2.1 --- a/doc-src/IsarRef/Thy/document/Misc.tex	Tue Jun 03 00:03:52 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Misc.tex	Tue Jun 03 00:03:54 2008 +0200
     2.3 @@ -235,7 +235,7 @@
     2.4  \end{isamarkuptext}%
     2.5  \isamarkuptrue%
     2.6  %
     2.7 -\isamarkupsection{System operations%
     2.8 +\isamarkupsection{System commands%
     2.9  }
    2.10  \isamarkuptrue%
    2.11  %
     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Tue Jun 03 00:03:52 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Tue Jun 03 00:03:54 2008 +0200
     3.3 @@ -713,18 +713,12 @@
     3.4  \end{isamarkuptext}%
     3.5  \isamarkuptrue%
     3.6  %
     3.7 -\isamarkupsection{Axiomatic type classes \label{sec:axclass}%
     3.8 +\isamarkupsubsection{Old-style axiomatic type classes \label{sec:axclass}%
     3.9  }
    3.10  \isamarkuptrue%
    3.11  %
    3.12  \begin{isamarkuptext}%
    3.13 -\begin{warn}
    3.14 -  This describes the old interface to axiomatic type-classes in
    3.15 -  Isabelle.  See \secref{sec:class} for a more recent higher-level
    3.16 -  view on the same ideas.
    3.17 -  \end{warn}
    3.18 -
    3.19 -  \begin{matharray}{rcl}
    3.20 +\begin{matharray}{rcl}
    3.21      \indexdef{}{command}{axclass}\hypertarget{command.axclass}{\hyperlink{command.axclass}{\mbox{\isa{\isacommand{axclass}}}}} & : & \isartrans{theory}{theory} \\
    3.22      \indexdef{}{command}{instance}\hypertarget{command.instance}{\hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}} & : & \isartrans{theory}{proof(prove)} \\
    3.23    \end{matharray}