--- a/doc-src/AxClass/Group/document/Group.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/AxClass/Group/document/Group.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Group}%
-\isamarkupfalse%
%
\isamarkupheader{Basic group theory%
}
--- a/doc-src/AxClass/Group/document/Product.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/AxClass/Group/document/Product.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Product}%
-\isamarkupfalse%
%
\isamarkupheader{Syntactic classes%
}
--- a/doc-src/AxClass/Group/document/Semigroups.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/AxClass/Group/document/Semigroups.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Semigroups}%
-\isamarkupfalse%
%
\isamarkupheader{Semigroups%
}
--- a/doc-src/AxClass/Nat/document/NatClass.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/AxClass/Nat/document/NatClass.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{NatClass}%
-\isamarkupfalse%
%
\isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}%
}
--- a/doc-src/IsarOverview/Isar/document/Induction.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/Induction.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Induction}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/IsarOverview/Isar/document/Logic.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Logic}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/Locales/Locales/document/Locales.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/Locales/Locales/document/Locales.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Locales}%
-\isamarkupfalse%
%
\isadelimtheory
\isanewline
--- a/doc-src/TutorialI/Advanced/document/Partial.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Partial}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Advanced/document/WFrec.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{WFrec}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Advanced/document/simp.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Advanced/document/simp.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{simp}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/CTL/document/Base.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/Base.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Base}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/CTL/document/CTL.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/CTL.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{CTL}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/CTL/document/CTLind.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/CTLind.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{CTLind}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/CTL/document/PDL.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/CTL/document/PDL.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{PDL}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{CodeGen}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{ABexpr}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Fundata}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Datatype/document/Nested.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Nested}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{unfoldnested}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Documents/document/Documents.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Documents}%
-\isamarkupfalse%
%
\isadelimtheory
%
@@ -134,26 +133,24 @@
printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is
output as \isa{A\isactrlsup {\isasymstar}}.
- A number of symbols are considered letters by the Isabelle lexer
- and can be used as part of identifiers. These are the greek letters
- \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}, etc apart from
- \isa{{\isasymlambda}}, caligraphic letters like \isa{{\isasymA}}
- (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+),
- and the special control symbols \verb+\+\verb+<^isub>+ and
- \verb+\+\verb+<^isup>+ for single letter sub and super scripts. This
- means that the input
+ A number of symbols are considered letters by the Isabelle lexer and
+ can be used as part of identifiers. These are the greek letters
+ \isa{{\isasymalpha}} (\verb+\+\verb+<alpha>+), \isa{{\isasymbeta}}
+ (\verb+\+\verb+<beta>+), etc. (excluding \isa{{\isasymlambda}}),
+ special letters like \isa{{\isasymA}} (\verb+\+\verb+<A>+) and \isa{{\isasymAA}} (\verb+\+\verb+<AA>+), and the control symbols
+ \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
+ sub and super scripts. This means that the input
\medskip
- {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.\,\verb,<alpha>\<^isub>1=\,\verb,<Pi>\<^isup>\<A>,}
+ {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
\medskip
\noindent is recognized as the term \isa{{\isasymforall}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isachardot}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isacharequal}\ {\isasymPi}\isactrlisup {\isasymA}}
- by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single entity like
- \isa{PA}, not an exponentiation.
+ by Isabelle. Note that \isa{{\isasymPi}\isactrlisup {\isasymA}} is a single
+ syntactic entity, not an exponentiation.
-
- \medskip Replacing our definition of \isa{xor} by the following
- specifies an Isabelle symbol for the new operator:%
+ \medskip Replacing our previous definition of \isa{xor} by the
+ following specifies an Isabelle symbol for the new operator:%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -425,10 +422,7 @@
location of the ultimate results. The above dry run should be able
to produce some \texttt{document.pdf} (with dummy title, empty table
of contents etc.). Any failure at this stage usually indicates
- technical problems of the {\LaTeX} installation.\footnote{Especially
- make sure that \texttt{pdflatex} is present; if in doubt one may
- fall back on DVI output by changing \texttt{usedir} options in
- \texttt{IsaMakefile} \cite{isabelle-sys}.}
+ technical problems of the {\LaTeX} installation.
\medskip The detailed arrangement of the session sources is as
follows.
@@ -826,37 +820,54 @@
no_document use_thy "T";
\end{verbatim}
- \medskip Theory output may be suppressed more selectively. Research
- articles and slides usually do not include the formal content in
- full. Delimiting \bfindex{ignored material} by the special source
- comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
- \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document
- preparation system to suppress these parts; the formal checking of
- the theory is unchanged, of course.
-
- In this example, we hide a theory's \isakeyword{theory} and
- \isakeyword{end} brackets:
-
- \medskip
+ \medskip Theory output may be suppressed more selectively, either
+ via \bfindex{tagged command regions} or \bfindex{ignored material}.
- \begin{tabular}{l}
- \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
- \texttt{theory T} \\
- \texttt{imports Main} \\
- \texttt{begin} \\
- \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
- ~~$\vdots$ \\
- \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\
- \texttt{end} \\
- \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\
- \end{tabular}
+ Tagged command regions works by annotating commands with named tags,
+ which correspond to certain {\LaTeX} markup that tells how to treat
+ particular parts of a document when doing the actual type-setting.
+ By default, certain Isabelle/Isar commands are implicitly marked up
+ using the predefined tags ``\emph{theory}'' (for theory begin and
+ end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for
+ commands involving ML code). Users may add their own tags using the
+ \verb,%,\emph{tag} notation right after a command name. In the
+ subsequent example we hide a particularly irrelevant proof:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isacharequal}\ x{\isachardoublequoteclose}%
+\isadeliminvisible
+\ %
+\endisadeliminvisible
+%
+\isataginvisible
+\isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}simp{\isacharparenright}%
+\endisataginvisible
+{\isafoldinvisible}%
+%
+\isadeliminvisible
+%
+\endisadeliminvisible
+%
+\begin{isamarkuptext}%
+The original source has been ``\verb,lemma "x = x" by %invisible (simp),''.
+ Tags observe the structure of proofs; adjacent commands with the
+ same tag are joined into a single region. The Isabelle document
+ preparation system allows the user to specify how to interpret a
+ tagged region, in order to keep, drop, or fold the corresponding
+ parts of the document. See the \emph{Isabelle System Manual}
+ \cite{isabelle-sys} for further details, especially on
+ \texttt{isatool usedir} and \texttt{isatool document}.
- \medskip
-
- Text may be suppressed in a fine-grained manner. We may even hide
- vital parts of a proof, pretending that things have been simpler
- than they really were. For example, this ``fully automatic'' proof
- is actually a fake:%
+ Ignored material is specified by delimiting the original formal
+ source with special source comments
+ \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and
+ \verb,(,\verb,*,\verb,>,\verb,*,\verb,),. These parts are stripped
+ before the type-setting phase, without affecting the formal checking
+ of the theory, of course. For example, we may hide parts of a proof
+ that seem unfit for general public inspection. The following
+ ``fully automatic'' proof is actually a fake:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
@@ -877,7 +888,7 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Here the real source of the proof has been as follows:
+\noindent The real source of the proof has been as follows:
\begin{verbatim}
by (auto(*<*)simp add: zero_less_mult_iff(*>*))
@@ -887,23 +898,7 @@
\medskip Suppressing portions of printed text demands care. You
should not misrepresent the underlying theory development. It is
easy to invalidate the visible text by hiding references to
- questionable axioms.
-
-% I removed this because the page overflowed and I disagree a little. TN
-%
-% Authentic reports of Isabelle/Isar theories, say as part of a
-% library, should suppress nothing. Other users may need the full
-% information for their own derivative work. If a particular
-% formalization appears inadequate for general public coverage, it is
-% often more appropriate to think of a better way in the first place.
-
- \medskip Some technical subtleties of the
- \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,),
- elements need to be kept in mind, too --- the system performs few
- sanity checks here. Arguments of markup commands and formal
- comments must not be hidden, otherwise presentation fails. Open and
- close parentheses need to be inserted carefully; it is easy to hide
- the wrong parts, especially after rearranging the theory text.%
+ questionable axioms.%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Ifexpr}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Inductive/document/AB.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/AB.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{AB}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Advanced}%
-\isamarkupfalse%
%
\isadelimtheory
\isanewline
--- a/doc-src/TutorialI/Inductive/document/Even.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Even.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Even}%
-\isamarkupfalse%
%
\isadelimtheory
\isanewline
--- a/doc-src/TutorialI/Inductive/document/Mutual.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Mutual}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Inductive/document/Star.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Inductive/document/Star.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Star}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{AdvancedInd}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/Itrev.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Itrev}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/Option2.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Option2.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Option{\isadigit{2}}}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/Plus.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Plus.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Plus}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/Tree.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Tree}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/Tree2.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/Tree2.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Tree{\isadigit{2}}}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/appendix.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/appendix.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{appendix}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{case{\isacharunderscore}exprs}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/fakenat.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/fakenat.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{fakenat}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{natsum}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/pairs.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/pairs.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{pairs}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/prime_def.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{prime{\isacharunderscore}def}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/simp.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{simp}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Misc/document/types.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Misc/document/types.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{types}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Recdef/document/Induction.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Induction}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Recdef/document/Nested0.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Nested{\isadigit{0}}}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Nested{\isadigit{1}}}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Nested{\isadigit{2}}}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Recdef/document/examples.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/examples.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{examples}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Recdef/document/simplification.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{simplification}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Recdef/document/termination.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{termination}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Rules/document/find2.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Rules/document/find2.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{find{\isadigit{2}}}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{ToyList}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Trie/document/Trie.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Trie}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Types/document/Axioms.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Axioms}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Types/document/Numbers.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Numbers}%
-\isamarkupfalse%
%
\isadelimtheory
\isanewline
--- a/doc-src/TutorialI/Types/document/Overloading.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Overloading}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Overloading{\isadigit{0}}}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Overloading{\isadigit{1}}}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Overloading{\isadigit{2}}}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Types/document/Pairs.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Pairs}%
-\isamarkupfalse%
%
\isadelimtheory
%
--- a/doc-src/TutorialI/Types/document/Records.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Records.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Records}%
-\isamarkupfalse%
%
\isamarkupheader{Records \label{sec:records}%
}
--- a/doc-src/TutorialI/Types/document/Typedefs.tex Mon Aug 29 16:18:07 2005 +0200
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex Mon Aug 29 16:25:24 2005 +0200
@@ -1,7 +1,6 @@
%
\begin{isabellebody}%
\def\isabellecontext{Typedefs}%
-\isamarkupfalse%
%
\isadelimtheory
%