doc-src/IsarOverview/Isar/document/Logic.tex

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

 \isadelimML
 %
 \endisadelimML
 %
 \isatagML
-\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
 %
 \isadelimML

 goal. The corresponding Isar proof pattern (for $n = 3$) is very handy:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \renewcommand{\isamarkupcmt}[1]{#1}
-\isamarkupfalse%
 %
 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequoteclose}\ \isamarkupfalse%
-\ %
+\ {\isachardoublequoteopen}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequoteclose}\ \ %
 \isamarkupcmt{\dots%
 }
 \isanewline
 \ \ \isacommand{moreover}\isamarkupfalse%
 \isanewline

 \ \ \ \ %
 \isamarkupcmt{\dots%
 }
 \isanewline
 \ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isamarkupfalse%
-\ %
+\ {\isacharquery}thesis\ \ %
 \isamarkupcmt{\dots%
 }
 \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{moreover}\isamarkupfalse%

 \ \ \ \ %
 \isamarkupcmt{\dots%
 }
 \isanewline
 \ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isamarkupfalse%
-\ %
+\ {\isacharquery}thesis\ \ %
 \isamarkupcmt{\dots%
 }
 \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{moreover}\isamarkupfalse%

 \ \ \ \ %
 \isamarkupcmt{\dots%
 }
 \isanewline
 \ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isamarkupfalse%
-\ %
+\ {\isacharquery}thesis\ \ %
 \isamarkupcmt{\dots%
 }
 \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
 \isanewline
 \ \ \isacommand{ultimately}\isamarkupfalse%

 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof

 \isadelimproof
 %
 \endisadelimproof
 %
 \isatagproof
-\isamarkupfalse%
 %
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof

 \isacommand{proof}\isamarkupfalse%
 \ {\isacharminus}\isanewline
 \ \ \isacommand{from}\isamarkupfalse%
 \ A\ \isacommand{obtain}\isamarkupfalse%
 \ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequoteopen}P\ x\ y{\isachardoublequoteclose}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequoteopen}Q\ x\ y{\isachardoublequoteclose}\ \ \isacommand{by}\isamarkupfalse%
-\ blast\isamarkupfalse%
-%
+\ blast%
 \endisatagproof
 {\isafoldproof}%
 %
 \isadelimproof
 %

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