# HG changeset patch
# User paulson
# Date 973525299 -3600
# Node ID e2d0dda41f2c4d59f6a01e200cda7b216edc9f6a
# Parent  5ab08609e6c8c31fb7e060ebe60d772ad82296f9
auto update

diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- 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}
diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Misc/document/Itrev.tex
--- 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}
diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Misc/document/case_exprs.tex
--- 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}
diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Misc/document/simp.tex
--- 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}
diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Types/document/Axioms.tex
--- 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,
diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Types/document/Overloading0.tex
--- 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
diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Types/document/Overloading1.tex
--- 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
diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Types/document/Overloading2.tex
--- 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.
diff -r 5ab08609e6c8 -r e2d0dda41f2c doc-src/TutorialI/Types/document/Typedef.tex
--- 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}