--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Nov 06 16:41:39 2000 +0100
@@ -12,7 +12,8 @@
with an extended example of induction (\S\ref{sec:CTL-revisited}).%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Massaging the proposition}
+\isamarkupsubsection{Massaging the proposition%
+}
%
\begin{isamarkuptext}%
\label{sec:ind-var-in-prems}
@@ -123,7 +124,8 @@
the conclusion as well, under the \isa{{\isasymforall}}, again using \isa{{\isasymlongrightarrow}} as shown above.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Beyond structural and recursion induction}
+\isamarkupsubsection{Beyond structural and recursion induction%
+}
%
\begin{isamarkuptext}%
\label{sec:complete-ind}
@@ -241,7 +243,8 @@
\end{quote}%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Derivation of new induction schemas}
+\isamarkupsubsection{Derivation of new induction schemas%
+}
%
\begin{isamarkuptext}%
\label{sec:derive-ind}
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Mon Nov 06 16:41:39 2000 +0100
@@ -2,7 +2,8 @@
\begin{isabellebody}%
\def\isabellecontext{Itrev}%
%
-\isamarkupsection{Induction heuristics}
+\isamarkupsection{Induction heuristics%
+}
%
\begin{isamarkuptext}%
\label{sec:InductionHeuristics}
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Mon Nov 06 16:41:39 2000 +0100
@@ -2,7 +2,8 @@
\begin{isabellebody}%
\def\isabellecontext{case{\isacharunderscore}exprs}%
%
-\isamarkupsubsection{Case expressions}
+\isamarkupsubsection{Case expressions%
+}
%
\begin{isamarkuptext}%
\label{sec:case-expressions}
@@ -48,7 +49,8 @@
indicate their scope%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Structural induction and case distinction}
+\isamarkupsubsection{Structural induction and case distinction%
+}
%
\begin{isamarkuptext}%
\indexbold{structural induction}
--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Mon Nov 06 16:41:39 2000 +0100
@@ -2,7 +2,8 @@
\begin{isabellebody}%
\def\isabellecontext{simp}%
%
-\isamarkupsubsubsection{Simplification rules}
+\isamarkupsubsubsection{Simplification rules%
+}
%
\begin{isamarkuptext}%
\indexbold{simplification rule}
@@ -39,7 +40,8 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{The simplification method}
+\isamarkupsubsubsection{The simplification method%
+}
%
\begin{isamarkuptext}%
\index{*simp (method)|bold}
@@ -55,7 +57,8 @@
Note that \isa{simp} fails if nothing changes.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Adding and deleting simplification rules}
+\isamarkupsubsubsection{Adding and deleting simplification rules%
+}
%
\begin{isamarkuptext}%
If a certain theorem is merely needed in a few proofs by simplification,
@@ -73,7 +76,8 @@
\end{quote}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Assumptions}
+\isamarkupsubsubsection{Assumptions%
+}
%
\begin{isamarkuptext}%
\index{simplification!with/of assumptions}
@@ -123,7 +127,8 @@
other arguments.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Rewriting with definitions}
+\isamarkupsubsubsection{Rewriting with definitions%
+}
%
\begin{isamarkuptext}%
\index{simplification!with definitions}
@@ -171,7 +176,8 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Simplifying let-expressions}
+\isamarkupsubsubsection{Simplifying let-expressions%
+}
%
\begin{isamarkuptext}%
\index{simplification!of let-expressions}
@@ -190,7 +196,8 @@
default:%
\end{isamarkuptext}%
\isacommand{declare}\ Let{\isacharunderscore}def\ {\isacharbrackleft}simp{\isacharbrackright}%
-\isamarkupsubsubsection{Conditional equations}
+\isamarkupsubsubsection{Conditional equations%
+}
%
\begin{isamarkuptext}%
So far all examples of rewrite rules were equations. The simplifier also
@@ -217,7 +224,8 @@
assumption of the subgoal.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Automatic case splits}
+\isamarkupsubsubsection{Automatic case splits%
+}
%
\begin{isamarkuptext}%
\indexbold{case splits}\index{*split|(}
@@ -310,7 +318,8 @@
\index{*split|)}%
\end{isamarkuptxt}%
%
-\isamarkupsubsubsection{Arithmetic}
+\isamarkupsubsubsection{Arithmetic%
+}
%
\begin{isamarkuptext}%
\index{arithmetic}
@@ -330,7 +339,8 @@
is not proved by simplification and requires \isa{arith}.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Tracing}
+\isamarkupsubsubsection{Tracing%
+}
%
\begin{isamarkuptext}%
\indexbold{tracing the simplifier}
--- a/doc-src/TutorialI/Types/document/Axioms.tex Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Mon Nov 06 16:41:39 2000 +0100
@@ -2,7 +2,8 @@
\begin{isabellebody}%
\def\isabellecontext{Axioms}%
%
-\isamarkupsubsection{Axioms}
+\isamarkupsubsection{Axioms%
+}
%
\begin{isamarkuptext}%
Now we want to attach axioms to our classes. Then we can reason on the
@@ -11,7 +12,8 @@
our above ordering relations.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Partial orders}
+\isamarkupsubsubsection{Partial orders%
+}
%
\begin{isamarkuptext}%
A \emph{partial order} is a subclass of \isa{ordrel}
@@ -86,7 +88,8 @@
proof for each instance.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Linear orders}
+\isamarkupsubsubsection{Linear orders%
+}
%
\begin{isamarkuptext}%
If any two elements of a partial order are comparable it is a
@@ -112,7 +115,8 @@
section.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Strict orders}
+\isamarkupsubsubsection{Strict orders%
+}
%
\begin{isamarkuptext}%
An alternative axiomatization of partial orders takes \isa{{\isacharless}{\isacharless}} rather than
@@ -139,7 +143,8 @@
complain if you also prove the relationship \isa{strord\ {\isacharless}\ parord}.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Multiple inheritance and sorts}
+\isamarkupsubsubsection{Multiple inheritance and sorts%
+}
%
\begin{isamarkuptext}%
A class may inherit from more than one direct superclass. This is called
@@ -192,7 +197,8 @@
you base your own ordering relations on this theory.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Inconsistencies}
+\isamarkupsubsubsection{Inconsistencies%
+}
%
\begin{isamarkuptext}%
The reader may be wondering what happens if we, maybe accidentally,
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Mon Nov 06 16:41:39 2000 +0100
@@ -8,7 +8,8 @@
constant may have multiple definitions at non-overlapping types.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{An initial example}
+\isamarkupsubsubsection{An initial example%
+}
%
\begin{isamarkuptext}%
If we want to introduce the notion of an \emph{inverse} for arbitrary types we
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Mon Nov 06 16:41:39 2000 +0100
@@ -2,7 +2,8 @@
\begin{isabellebody}%
\def\isabellecontext{Overloading{\isadigit{1}}}%
%
-\isamarkupsubsubsection{Controlled overloading with type classes}
+\isamarkupsubsubsection{Controlled overloading with type classes%
+}
%
\begin{isamarkuptext}%
We now start with the theory of ordering relations, which we want to phrase
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Mon Nov 06 16:41:39 2000 +0100
@@ -19,7 +19,8 @@
The infix function \isa{{\isacharbang}} yields the nth element of a list.%
\end{isamarkuptext}%
%
-\isamarkupsubsubsection{Predefined overloading}
+\isamarkupsubsubsection{Predefined overloading%
+}
%
\begin{isamarkuptext}%
HOL comes with a number of overloaded constants and corresponding classes.
--- a/doc-src/TutorialI/Types/document/Typedef.tex Mon Nov 06 11:32:23 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex Mon Nov 06 16:41:39 2000 +0100
@@ -2,7 +2,8 @@
\begin{isabellebody}%
\def\isabellecontext{Typedef}%
%
-\isamarkupsection{Introducing new types}
+\isamarkupsection{Introducing new types%
+}
%
\begin{isamarkuptext}%
\label{sec:adv-typedef}
@@ -18,7 +19,8 @@
\end{warn}%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Declaring new types}
+\isamarkupsubsection{Declaring new types%
+}
%
\begin{isamarkuptext}%
\label{sec:typedecl}
@@ -55,7 +57,8 @@
unnecessary: a one-element type called \isa{unit} is already defined in HOL.%
\end{isamarkuptext}%
%
-\isamarkupsubsection{Defining new types}
+\isamarkupsubsection{Defining new types%
+}
%
\begin{isamarkuptext}%
\label{sec:typedef}