updated;

--- a/doc-src/AxClass/generated/Group.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/AxClass/generated/Group.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{Group}%
 %
-\isamarkupheader{Basic group theory}
+\isamarkupheader{Basic group theory%
+}
 \isacommand{theory}\ Group\ {\isacharequal}\ Main{\isacharcolon}%
 \begin{isamarkuptext}%
 \medskip\noindent The meta-level type system of Isabelle supports
@@ -14,7 +15,8 @@
  general groups and Abelian groups.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Monoids and Groups}
+\isamarkupsubsection{Monoids and Groups%
+}
 %
 \begin{isamarkuptext}%
 First we declare some polymorphic constants required later for the
@@ -64,7 +66,8 @@
  is even commutative.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Abstract reasoning}
+\isamarkupsubsection{Abstract reasoning%
+}
 %
 \begin{isamarkuptext}%
 In a sense, axiomatic type classes may be viewed as \emph{abstract
@@ -124,7 +127,8 @@
  known at Isabelle's type signature level.  Since we have \isa{agroup\ {\isasymsubseteq}\ group\ {\isasymsubseteq}\ semigroup} by definition, all theorems of \isa{semigroup} and \isa{group} are automatically inherited by \isa{group} and \isa{agroup}.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Abstract instantiation}
+\isamarkupsubsection{Abstract instantiation%
+}
 %
 \begin{isamarkuptext}%
 From the definition, the \isa{monoid} and \isa{group} classes
@@ -191,7 +195,8 @@
  hierarchy.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}}
+\isamarkupsubsection{Concrete instantiation \label{sec:inst-arity}%
+}
 %
 \begin{isamarkuptext}%
 So far we have covered the case of the form $\INSTANCE$~\isa{c\isactrlsub {\isadigit{1}}\ {\isacharless}\ c\isactrlsub {\isadigit{2}}}, namely \emph{abstract instantiation} ---
@@ -250,7 +255,8 @@
  types.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Lifting and Functors}
+\isamarkupsubsection{Lifting and Functors%
+}
 %
 \begin{isamarkuptext}%
 As already mentioned above, overloading in the simply-typed HOL

--- a/doc-src/AxClass/generated/NatClass.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/AxClass/generated/NatClass.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{NatClass}%
 %
-\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}}
+\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}%
+}
 \isacommand{theory}\ NatClass\ {\isacharequal}\ FOL{\isacharcolon}%
 \begin{isamarkuptext}%
 \medskip\noindent Axiomatic type classes abstract over exactly one

--- a/doc-src/AxClass/generated/Product.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/AxClass/generated/Product.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{Product}%
 %
-\isamarkupheader{Syntactic classes}
+\isamarkupheader{Syntactic classes%
+}
 \isacommand{theory}\ Product\ {\isacharequal}\ Main{\isacharcolon}%
 \begin{isamarkuptext}%
 \medskip\noindent There is still a feature of Isabelle's type system

--- a/doc-src/AxClass/generated/Semigroups.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/AxClass/generated/Semigroups.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{Semigroups}%
 %
-\isamarkupheader{Semigroups}
+\isamarkupheader{Semigroups%
+}
 \isacommand{theory}\ Semigroups\ {\isacharequal}\ Main{\isacharcolon}%
 \begin{isamarkuptext}%
 \medskip\noindent An axiomatic type class is simply a class of types

--- a/doc-src/TutorialI/Advanced/document/simp.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Advanced/document/simp.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{simp}%
 %
-\isamarkupsection{Simplification}
+\isamarkupsection{Simplification%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:simplification-II}\index{simplification|(}
@@ -12,9 +13,11 @@
 situation.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Advanced features}
+\isamarkupsubsection{Advanced features%
+}
 %
-\isamarkupsubsubsection{Congruence rules}
+\isamarkupsubsubsection{Congruence rules%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:simp-cong}
@@ -75,7 +78,8 @@
 \end{warn}%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Permutative rewrite rules}
+\isamarkupsubsubsection{Permutative rewrite rules%
+}
 %
 \begin{isamarkuptext}%
 \index{rewrite rule!permutative|bold}
@@ -120,7 +124,8 @@
 this.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{How it works}
+\isamarkupsubsection{How it works%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:SimpHow}
@@ -129,7 +134,8 @@
 proved (again by simplification). Below we explain some special features of the rewriting process.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{Higher-order patterns}
+\isamarkupsubsubsection{Higher-order patterns%
+}
 %
 \begin{isamarkuptext}%
 \index{simplification rule|(}
@@ -167,7 +173,8 @@
 sides.  They may not contain extraneous term or type variables, though.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{The preprocessor}
+\isamarkupsubsubsection{The preprocessor%
+}
 %
 \begin{isamarkuptext}%
 When some theorem is declared a simplification rule, it need not be a

--- a/doc-src/TutorialI/CTL/document/Base.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{Base}%
 %
-\isamarkupsection{Case study: Verified model checking}
+\isamarkupsection{Case study: Verified model checking%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:VMC}

--- a/doc-src/TutorialI/CTL/document/CTL.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{CTL}%
 %
-\isamarkupsubsection{Computation tree logic---CTL}
+\isamarkupsubsection{Computation tree logic---CTL%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:CTL}

--- a/doc-src/TutorialI/CTL/document/CTLind.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{CTLind}%
 %
-\isamarkupsubsection{CTL revisited}
+\isamarkupsubsection{CTL revisited%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:CTL-revisited}

--- a/doc-src/TutorialI/CTL/document/PDL.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{PDL}%
 %
-\isamarkupsubsection{Propositional dynamic logic---PDL}
+\isamarkupsubsection{Propositional dynamic logic---PDL%
+}
 %
 \begin{isamarkuptext}%
 \index{PDL|(}

--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{CodeGen}%
 %
-\isamarkupsection{Case study: compiling expressions}
+\isamarkupsection{Case study: compiling expressions%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:ExprCompiler}

--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{Ifexpr}%
 %
-\isamarkupsubsection{Case study: boolean expressions}
+\isamarkupsubsection{Case study: boolean expressions%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:boolex}
@@ -11,7 +12,8 @@
 the constructs introduced above.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{How can we model boolean expressions?}
+\isamarkupsubsubsection{How can we model boolean expressions?%
+}
 %
 \begin{isamarkuptext}%
 We want to represent boolean expressions built up from variables and

--- a/doc-src/TutorialI/Inductive/document/AB.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/AB.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{AB}%
 %
-\isamarkupsection{Case study: A context free grammar}
+\isamarkupsection{Case study: A context free grammar%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:CFG}

--- a/doc-src/TutorialI/Inductive/document/Star.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/Star.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -2,7 +2,8 @@
 \begin{isabellebody}%
 \def\isabellecontext{Star}%
 %
-\isamarkupsection{The reflexive transitive closure}
+\isamarkupsection{The reflexive transitive closure%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:rtc}

--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -11,7 +11,8 @@
 examples of induction.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsection{Massaging the proposition}
+\isamarkupsubsection{Massaging the proposition%
+}
 %
 \begin{isamarkuptext}%
 \label{sec:ind-var-in-prems}
@@ -122,7 +123,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}
@@ -240,7 +242,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	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Sat Nov 04 18:54:22 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	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Sat Nov 04 18:54:22 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	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Sat Nov 04 18:54:22 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/ToyList/document/ToyList.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Sat Nov 04 18:54:22 2000 +0100
@@ -208,7 +208,8 @@
 In order to simplify this subgoal further, a lemma suggests itself.%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{First lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}}
+\isamarkupsubsubsection{First lemma: \isa{rev{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}rev\ ys{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}rev\ xs{\isacharparenright}}%
+}
 %
 \begin{isamarkuptext}%
 After abandoning the above proof attempt\indexbold{abandon
@@ -242,7 +243,8 @@
 embarking on the proof of a lemma usually remains implicit.%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}}
+\isamarkupsubsubsection{Second lemma: \isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs}%
+}
 %
 \begin{isamarkuptext}%
 This time the canonical proof procedure%
@@ -296,7 +298,8 @@
 and the missing lemma is associativity of \isa{{\isacharat}}.%
 \end{isamarkuptxt}%
 %
-\isamarkupsubsubsection{Third lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}}
+\isamarkupsubsubsection{Third lemma: \isa{{\isacharparenleft}xs\ {\isacharat}\ ys{\isacharparenright}\ {\isacharat}\ zs\ {\isacharequal}\ xs\ {\isacharat}\ {\isacharparenleft}ys\ {\isacharat}\ zs{\isacharparenright}}%
+}
 %
 \begin{isamarkuptext}%
 Abandoning the previous proof, the canonical proof procedure%

--- a/doc-src/TutorialI/Types/document/Axioms.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex	Sat Nov 04 18:54:22 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
@@ -160,7 +164,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	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex	Sat Nov 04 18:54:22 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	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex	Sat Nov 04 18:54:22 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/Typedef.tex	Sat Nov 04 18:44:34 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex	Sat Nov 04 18:54:22 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}