author wenzelm Sat, 04 Nov 2000 18:54:22 +0100 changeset 10395 7ef380745743 parent 10394 eef9e422929a child 10396 5ab08609e6c8
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}%
%
+}
\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}%
%
+}
\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}%
%
+}
\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}%
%
+}
%
-\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}%
%
+}
%
\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
@@ -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
@@ -2,7 +2,8 @@
\begin{isabellebody}%
%
+}
%
\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}%
@@ -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}