doc-src/TutorialI/Types/document/Pairs.tex

 %
 \begin{isabellebody}%
 \def\isabellecontext{Pairs}%
+\isamarkupfalse%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
 %
 \isadelimtheory

 \end{isabelle}
 This subgoal is easily proved by simplification. Thus we could have combined
 simplification and splitting in one command that proves the goal outright:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
 %
 \isadelimproof
 %
 \endisadelimproof
 %

 \end{isabelle}
 A paired \isa{let} reduces to a paired $\lambda$-abstraction, which
 can be split as above. The same is true for paired set comprehension:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof

 as above. If you are worried about the strange form of the premise:
 \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}.
 The same proof procedure works for%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof

 
 However, splitting \isa{split} is not always a solution, as no \isa{split}
 may be present in the goal. Consider the following function:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof

 In case the term to be split is a quantified variable, there are more options.
 You can split \emph{all} \isa{{\isasymAnd}}-quantified variables in a goal
 with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof

 of the simplifier.
 The following command could fail (here it does not)
 where two separate \isa{simp} applications succeed.%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isamarkupfalse%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
-%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{apply}\isamarkupfalse%
+{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}%
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
 %

 \isadelimtheory
 %
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
 %
 \isadelimtheory