doc-src/TutorialI/Misc/document/simp.tex

--- a/doc-src/TutorialI/Misc/document/simp.tex	Thu Jul 26 16:54:44 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,799 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{simp}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsubsection{Simplification Rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\index{simplification rules}
-To facilitate simplification,  
-the attribute \isa{{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}}\index{*simp (attribute)}
-declares theorems to be simplification rules, which the simplifier
-will use automatically.  In addition, \isacommand{datatype} and
-\isacommand{primrec} declarations (and a few others) 
-implicitly declare some simplification rules.  
-Explicit definitions are \emph{not} declared as 
-simplification rules automatically!
-
-Nearly any theorem can become a simplification
-rule. The simplifier will try to transform it into an equation.  
-For example, the theorem
-\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P} is turned into \isa{P\ {\isaliteral{3D}{\isacharequal}}\ False}. The details
-are explained in \S\ref{sec:SimpHow}.
-
-The simplification attribute of theorems can be turned on and off:%
-\index{*simp del (attribute)}
-\begin{quote}
-\isacommand{declare} \textit{theorem-name}\isa{{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}}\\
-\isacommand{declare} \textit{theorem-name}\isa{{\isaliteral{5B}{\isacharbrackleft}}simp\ del{\isaliteral{5D}{\isacharbrackright}}}
-\end{quote}
-Only equations that really simplify, like \isa{rev\
-{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs} and
-\isa{xs\ {\isacharat}\ {\isacharbrackleft}{\isacharbrackright}\
-{\isacharequal}\ xs}, should be declared as default simplification rules. 
-More specific ones should only be used selectively and should
-not be made default.  Distributivity laws, for example, alter
-the structure of terms and can produce an exponential blow-up instead of
-simplification.  A default simplification rule may
-need to be disabled in certain proofs.  Frequent changes in the simplification
-status of a theorem may indicate an unwise use of defaults.
-\begin{warn}
-  Simplification can run forever, for example if both $f(x) = g(x)$ and
-  $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
-  to include simplification rules that can lead to nontermination, either on
-  their own or in combination with other simplification rules.
-\end{warn}
-\begin{warn}
-  It is inadvisable to toggle the simplification attribute of a
-  theorem from a parent theory $A$ in a child theory $B$ for good.
-  The reason is that if some theory $C$ is based both on $B$ and (via a
-  different path) on $A$, it is not defined what the simplification attribute
-  of that theorem will be in $C$: it could be either.
-\end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{The {\tt\slshape simp}  Method%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\index{*simp (method)|bold}
-The general format of the simplification method is
-\begin{quote}
-\isa{simp} \textit{list of modifiers}
-\end{quote}
-where the list of \emph{modifiers} fine tunes the behaviour and may
-be empty. Specific modifiers are discussed below.  Most if not all of the
-proofs seen so far could have been performed
-with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks
-only the first subgoal and may thus need to be repeated --- use
-\methdx{simp_all} to simplify all subgoals.
-If nothing changes, \isa{simp} fails.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Adding and Deleting Simplification Rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\index{simplification rules!adding and deleting}%
-If a certain theorem is merely needed in a few proofs by simplification,
-we do not need to make it a global simplification rule. Instead we can modify
-the set of simplification rules used in a simplification step by adding rules
-to it and/or deleting rules from it. The two modifiers for this are
-\begin{quote}
-\isa{add{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}\index{*add (modifier)}\\
-\isa{del{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}\index{*del (modifier)}
-\end{quote}
-Or you can use a specific list of theorems and omit all others:
-\begin{quote}
-\isa{only{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names}\index{*only (modifier)}
-\end{quote}
-In this example, we invoke the simplifier, adding two distributive
-laws:
-\begin{quote}
-\isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ mod{\isaliteral{5F}{\isacharunderscore}}mult{\isaliteral{5F}{\isacharunderscore}}distrib\ add{\isaliteral{5F}{\isacharunderscore}}mult{\isaliteral{5F}{\isacharunderscore}}distrib{\isaliteral{29}{\isacharparenright}}}
-\end{quote}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Assumptions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\index{simplification!with/of assumptions}
-By default, assumptions are part of the simplification process: they are used
-as simplification rules and are simplified themselves. For example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ xs\ {\isaliteral{40}{\isacharat}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ ys\ {\isaliteral{40}{\isacharat}}\ xs{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ zs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-\ simp\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-The second assumption simplifies to \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, which in turn
-simplifies the first assumption to \isa{zs\ {\isaliteral{3D}{\isacharequal}}\ ys}, thus reducing the
-conclusion to \isa{ys\ {\isaliteral{3D}{\isacharequal}}\ ys} and hence to \isa{True}.
-
-In some cases, using the assumptions can lead to nontermination:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}g\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-An unmodified application of \isa{simp} loops.  The culprit is the
-simplification rule \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}g\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}, which is extracted from
-the assumption.  (Isabelle notices certain simple forms of
-nontermination but not this one.)  The problem can be circumvented by
-telling the simplifier to ignore the assumptions:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ {\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-Three modifiers influence the treatment of assumptions:
-\begin{description}
-\item[\isa{{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}}]\index{*no_asm (modifier)}
- means that assumptions are completely ignored.
-\item[\isa{{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}}]\index{*no_asm_simp (modifier)}
- means that the assumptions are not simplified but
-  are used in the simplification of the conclusion.
-\item[\isa{{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{5F}{\isacharunderscore}}use{\isaliteral{29}{\isacharparenright}}}]\index{*no_asm_use (modifier)}
- means that the assumptions are simplified but are not
-  used in the simplification of each other or the conclusion.
-\end{description}
-Only one of the modifiers is allowed, and it must precede all
-other modifiers.
-%\begin{warn}
-%Assumptions are simplified in a left-to-right fashion. If an
-%assumption can help in simplifying one to the left of it, this may get
-%overlooked. In such cases you have to rotate the assumptions explicitly:
-%\isacommand{apply}@ {text"("}\methdx{rotate_tac}~$n$@ {text")"}
-%causes a cyclic shift by $n$ positions from right to left, if $n$ is
-%positive, and from left to right, if $n$ is negative.
-%Beware that such rotations make proofs quite brittle.
-%\end{warn}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Rewriting with Definitions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:Simp-with-Defs}\index{simplification!with definitions}
-Constant definitions (\S\ref{sec:ConstDefinitions}) can be used as
-simplification rules, but by default they are not: the simplifier does not
-expand them automatically.  Definitions are intended for introducing abstract
-concepts and not merely as abbreviations.  Of course, we need to expand
-the definition initially, but once we have proved enough abstract properties
-of the new constant, we can forget its original definition.  This style makes
-proofs more robust: if the definition has to be changed,
-only the proofs of the abstract properties will be affected.
-
-For example, given%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{definition}\isamarkupfalse%
-\ xor\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}xor\ A\ B\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent
-we may want to prove%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}xor\ A\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}A{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-Typically, we begin by unfolding some definitions:
-\indexbold{definitions!unfolding}%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ only{\isaliteral{3A}{\isacharcolon}}\ xor{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptxt}%
-\noindent
-In this particular case, the resulting goal
-\begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A%
-\end{isabelle}
-can be proved by simplification. Thus we could have proved the lemma outright by%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ xor{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-Of course we can also unfold definitions in the middle of a proof.
-
-\begin{warn}
-  If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
-  occurrences of $f$ with at least two arguments. This may be helpful for unfolding
-  $f$ selectively, but it may also get in the way. Defining
-  $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
-\end{warn}
-
-There is also the special method \isa{unfold}\index{*unfold (method)|bold}
-which merely unfolds
-one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
-This is can be useful in situations where \isa{simp} does too much.
-Warning: \isa{unfold} acts on all subgoals!%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Simplifying {\tt\slshape let}-Expressions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\index{simplification!of \isa{let}-expressions}\index{*let expressions}%
-Proving a goal containing \isa{let}-expressions almost invariably requires the
-\isa{let}-con\-structs to be expanded at some point. Since
-\isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for
-the predefined constant \isa{Let}, expanding \isa{let}-constructs
-means rewriting with \tdx{Let_def}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}let\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ in\ xs{\isaliteral{40}{\isacharat}}ys{\isaliteral{40}{\isacharat}}xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ Let{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-If, in a particular context, there is no danger of a combinatorial explosion
-of nested \isa{let}s, you could even simplify with \isa{Let{\isaliteral{5F}{\isacharunderscore}}def} by
-default:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{declare}\isamarkupfalse%
-\ Let{\isaliteral{5F}{\isacharunderscore}}def\ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}%
-\isamarkupsubsection{Conditional Simplification Rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\index{conditional simplification rules}%
-So far all examples of rewrite rules were equations. The simplifier also
-accepts \emph{conditional} equations, for example%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ hd{\isaliteral{5F}{\isacharunderscore}}Cons{\isaliteral{5F}{\isacharunderscore}}tl{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ hd\ xs\ {\isaliteral{23}{\isacharhash}}\ tl\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}case{\isaliteral{5F}{\isacharunderscore}}tac\ xs{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{2C}{\isacharcomma}}\ simp{\isaliteral{29}{\isacharparenright}}\isanewline
-\isacommand{done}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
-sequence of methods. Assuming that the simplification rule
-\isa{{\isaliteral{28}{\isacharparenleft}}rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}}
-is present as well,
-the lemma below is proved by plain simplification:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ tl{\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-The conditional equation \isa{hd{\isaliteral{5F}{\isacharunderscore}}Cons{\isaliteral{5F}{\isacharunderscore}}tl} above
-can simplify \isa{hd\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{23}{\isacharhash}}\ tl\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}} to \isa{rev\ xs}
-because the corresponding precondition \isa{rev\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}
-simplifies to \isa{xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, which is exactly the local
-assumption of the subgoal.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Automatic Case Splits%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\label{sec:AutoCaseSplits}\indexbold{case splits}%
-Goals containing \isa{if}-expressions\index{*if expressions!splitting of}
-are usually proved by case
-distinction on the boolean condition.  Here is an example:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}xs{\isaliteral{2E}{\isachardot}}\ if\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ then\ rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ else\ rev\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\begin{isamarkuptxt}%
-\noindent
-The goal can be split by a special method, \methdx{split}:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}split\ split{\isaliteral{5F}{\isacharunderscore}}if{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptxt}%
-\noindent
-\begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}xs{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ rev\ xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-where \tdx{split_if} is a theorem that expresses splitting of
-\isa{if}s. Because
-splitting the \isa{if}s is usually the right proof strategy, the
-simplifier does it automatically.  Try \isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}}
-on the initial goal above.
-
-This splitting idea generalizes from \isa{if} to \sdx{case}.
-Let us simplify a case analysis over lists:\index{*list.split (theorem)}%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}case\ xs\ of\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ zs\ {\isaliteral{7C}{\isacharbar}}\ y{\isaliteral{23}{\isacharhash}}ys\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ y{\isaliteral{23}{\isacharhash}}{\isaliteral{28}{\isacharparenleft}}ys{\isaliteral{40}{\isacharat}}zs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{40}{\isacharat}}zs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}split\ list{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptxt}%
-\begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ zs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline
-\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ }{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}a\ list{\isaliteral{2E}{\isachardot}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{23}{\isacharhash}}\ list\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ a\ {\isaliteral{23}{\isacharhash}}\ list\ {\isaliteral{40}{\isacharat}}\ zs\ {\isaliteral{3D}{\isacharequal}}\ xs\ {\isaliteral{40}{\isacharat}}\ zs{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-The simplifier does not split
-\isa{case}-expressions, as it does \isa{if}-expressions, 
-because with recursive datatypes it could lead to nontermination.
-Instead, the simplifier has a modifier
-\isa{split}\index{*split (modifier)} 
-for adding splitting rules explicitly.  The
-lemma above can be proved in one step by%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ split{\isaliteral{3A}{\isacharcolon}}\ list{\isaliteral{2E}{\isachardot}}split{\isaliteral{29}{\isacharparenright}}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-whereas \isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}} alone will not succeed.
-
-Every datatype $t$ comes with a theorem
-$t$\isa{{\isaliteral{2E}{\isachardot}}split} which can be declared to be a \bfindex{split rule} either
-locally as above, or by giving it the \attrdx{split} attribute globally:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{declare}\isamarkupfalse%
-\ list{\isaliteral{2E}{\isachardot}}split\ {\isaliteral{5B}{\isacharbrackleft}}split{\isaliteral{5D}{\isacharbrackright}}%
-\begin{isamarkuptext}%
-\noindent
-The \isa{split} attribute can be removed with the \isa{del} modifier,
-either locally%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp\ split\ del{\isaliteral{3A}{\isacharcolon}}\ split{\isaliteral{5F}{\isacharunderscore}}if{\isaliteral{29}{\isacharparenright}}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-or globally:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{declare}\isamarkupfalse%
-\ list{\isaliteral{2E}{\isachardot}}split\ {\isaliteral{5B}{\isacharbrackleft}}split\ del{\isaliteral{5D}{\isacharbrackright}}%
-\begin{isamarkuptext}%
-Polished proofs typically perform splitting within \isa{simp} rather than 
-invoking the \isa{split} method.  However, if a goal contains
-several \isa{if} and \isa{case} expressions, 
-the \isa{split} method can be
-helpful in selectively exploring the effects of splitting.
-
-The split rules shown above are intended to affect only the subgoal's
-conclusion.  If you want to split an \isa{if} or \isa{case}-expression
-in the assumptions, you have to apply \tdx{split_if_asm} or
-$t$\isa{{\isaliteral{2E}{\isachardot}}split{\isaliteral{5F}{\isacharunderscore}}asm}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}if\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ then\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ else\ ys\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}split\ split{\isaliteral{5F}{\isacharunderscore}}if{\isaliteral{5F}{\isacharunderscore}}asm{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptxt}%
-\noindent
-Unlike splitting the conclusion, this step creates two
-separate subgoals, which here can be solved by \isa{simp{\isaliteral{5F}{\isacharunderscore}}all}:
-\begin{isabelle}%
-\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
-\ {\isadigit{2}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ ys\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}%
-\end{isabelle}
-If you need to split both in the assumptions and the conclusion,
-use $t$\isa{{\isaliteral{2E}{\isachardot}}splits} which subsumes $t$\isa{{\isaliteral{2E}{\isachardot}}split} and
-$t$\isa{{\isaliteral{2E}{\isachardot}}split{\isaliteral{5F}{\isacharunderscore}}asm}. Analogously, there is \isa{if{\isaliteral{5F}{\isacharunderscore}}splits}.
-
-\begin{warn}
-  The simplifier merely simplifies the condition of an 
-  \isa{if}\index{*if expressions!simplification of} but not the
-  \isa{then} or \isa{else} parts. The latter are simplified only after the
-  condition reduces to \isa{True} or \isa{False}, or after splitting. The
-  same is true for \sdx{case}-expressions: only the selector is
-  simplified at first, until either the expression reduces to one of the
-  cases or it is split.
-\end{warn}%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isamarkupsubsection{Tracing%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\indexbold{tracing the simplifier}
-Using the simplifier effectively may take a bit of experimentation.  Set the
-Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier} to get a better idea of what is going on:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}rev\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{29}{\isacharparenright}}%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-produces the following trace in Proof General's \pgmenu{Trace} buffer:
-
-\begin{ttbox}\makeatother
-[1]Applying instance of rewrite rule "List.rev.simps_2":
-rev (?x1 # ?xs1) \(\equiv\) rev ?xs1 @ [?x1]
-
-[1]Rewriting:
-rev [a] \(\equiv\) rev [] @ [a]
-
-[1]Applying instance of rewrite rule "List.rev.simps_1":
-rev [] \(\equiv\) []
-
-[1]Rewriting:
-rev [] \(\equiv\) []
-
-[1]Applying instance of rewrite rule "List.op @.append_Nil":
-[] @ ?y \(\equiv\) ?y
-
-[1]Rewriting:
-[] @ [a] \(\equiv\) [a]
-
-[1]Applying instance of rewrite rule
-?x2 # ?t1 = ?t1 \(\equiv\) False
-
-[1]Rewriting:
-[a] = [] \(\equiv\) False
-\end{ttbox}
-The trace lists each rule being applied, both in its general form and
-the instance being used. The \texttt{[}$i$\texttt{]} in front (where
-above $i$ is always \texttt{1}) indicates that we are inside the $i$th
-invocation of the simplifier. Each attempt to apply a
-conditional rule shows the rule followed by the trace of the
-(recursive!) simplification of the conditions, the latter prefixed by
-\texttt{[}$i+1$\texttt{]} instead of \texttt{[}$i$\texttt{]}.
-Another source of recursive invocations of the simplifier are
-proofs of arithmetic formulae. By default, recursive invocations are not shown,
-you must increase the trace depth via \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgmenu{Trace Simplifier Depth}.
-
-Many other hints about the simplifier's actions may appear.
-
-In more complicated cases, the trace can be very lengthy.  Thus it is
-advisable to reset the \pgmenu{Trace Simplifier} flag after having
-obtained the desired trace.
-Since this is easily forgotten (and may have the unpleasant effect of
-swamping the interface with trace information), here is how you can switch
-the trace on locally in a proof:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{using}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5F}{\isacharunderscore}}trace{\isaliteral{3D}{\isacharequal}}true{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
-\isacommand{apply}\isamarkupfalse%
-\ simp%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent
-Within the current proof, all simplifications in subsequent proof steps
-will be traced, but the text reminds you to remove the \isa{using} clause
-after it has done its job.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Finding Theorems\label{sec:find}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\indexbold{finding theorems}\indexbold{searching theorems}
-Isabelle's large database of proved theorems 
-offers a powerful search engine. Its chief limitation is
-its restriction to the theories currently loaded.
-
-\begin{pgnote}
-The search engine is started by clicking on Proof General's \pgmenu{Find} icon.
-You specify your search textually in the input buffer at the bottom
-of the window.
-\end{pgnote}
-
-The simplest form of search finds theorems containing specified
-patterns.  A pattern can be any term (even
-a single identifier).  It may contain ``\texttt{\_}'', a wildcard standing
-for any term. Here are some
-examples:
-\begin{ttbox}
-length
-"_ # _ = _ # _"
-"_ + _"
-"_ * (_ - (_::nat))"
-\end{ttbox}
-Specifying types, as shown in the last example, 
-constrains searches involving overloaded operators.
-
-\begin{warn}
-Always use ``\texttt{\_}'' rather than variable names: searching for
-\texttt{"x + y"} will usually not find any matching theorems
-because they would need to contain \texttt{x} and~\texttt{y} literally.
-When searching for infix operators, do not just type in the symbol,
-such as~\texttt{+}, but a proper term such as \texttt{"_ + _"}.
-This remark applies to more complicated syntaxes, too.
-\end{warn}
-
-If you are looking for rewrite rules (possibly conditional) that could
-simplify some term, prefix the pattern with \texttt{simp:}.
-\begin{ttbox}
-simp: "_ * (_ + _)"
-\end{ttbox}
-This finds \emph{all} equations---not just those with a \isa{simp} attribute---whose conclusion has the form
-\begin{isabelle}%
-\ \ \ \ \ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}%
-\end{isabelle}
-It only finds equations that can simplify the given pattern
-at the root, not somewhere inside: for example, equations of the form
-\isa{{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}} do not match.
-
-You may also search for theorems by name---you merely
-need to specify a substring. For example, you could search for all
-commutativity theorems like this:
-\begin{ttbox}
-name: comm
-\end{ttbox}
-This retrieves all theorems whose name contains \texttt{comm}.
-
-Search criteria can also be negated by prefixing them with ``\texttt{-}''.
-For example,
-\begin{ttbox}
--name: List
-\end{ttbox}
-finds theorems whose name does not contain \texttt{List}. You can use this
-to exclude particular theories from the search: the long name of
-a theorem contains the name of the theory it comes from.
-
-Finallly, different search criteria can be combined arbitrarily. 
-The effect is conjuctive: Find returns the theorems that satisfy all of
-the criteria. For example,
-\begin{ttbox}
-"_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
-\end{ttbox}
-looks for theorems containing plus but not minus, and which do not simplify
-\mbox{\isa{{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5F}{\isacharunderscore}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5F}{\isacharunderscore}}{\isaliteral{29}{\isacharparenright}}}} at the root, and whose name contains \texttt{assoc}.
-
-Further search criteria are explained in \S\ref{sec:find2}.
-
-\begin{pgnote}
-Proof General keeps a history of all your search expressions.
-If you click on \pgmenu{Find}, you can use the arrow keys to scroll
-through previous searches and just modify them. This saves you having
-to type in lengthy expressions again and again.
-\end{pgnote}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: