# HG changeset patch # User wenzelm # Date 1125308663 -7200 # Node ID 5f42dd5e657076c25dbe8772835f32760ba4d4b7 # Parent 5fefe658a6f8d92b74c7c10a35530cdfc397b35c updated; diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/AxClass/Group/document/Group.tex --- a/doc-src/AxClass/Group/document/Group.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/AxClass/Group/document/Group.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{Group}% +\isamarkupfalse% % \isamarkupheader{Basic group theory% } diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/AxClass/Group/document/Product.tex --- a/doc-src/AxClass/Group/document/Product.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/AxClass/Group/document/Product.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{Product}% +\isamarkupfalse% % \isamarkupheader{Syntactic classes% } diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/AxClass/Group/document/Semigroups.tex --- a/doc-src/AxClass/Group/document/Semigroups.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/AxClass/Group/document/Semigroups.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{Semigroups}% +\isamarkupfalse% % \isamarkupheader{Semigroups% } diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/AxClass/Group/document/isabelle.sty --- a/doc-src/AxClass/Group/document/isabelle.sty Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/AxClass/Group/document/isabelle.sty Mon Aug 29 11:44:23 2005 +0200 @@ -22,10 +22,10 @@ \newcommand{\isamath}[1]{\emph{$#1$}} \newcommand{\isatext}[1]{\emph{#1}} \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} -\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} @@ -89,6 +89,8 @@ \chardef\isacharbar=`\| \chardef\isacharbraceright=`\} \chardef\isachartilde=`\~ +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk} +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright} % keyword and section markup @@ -165,6 +167,8 @@ \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}% +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}% } \newcommand{\isabellestylesl}{% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/AxClass/Nat/document/NatClass.tex --- a/doc-src/AxClass/Nat/document/NatClass.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/AxClass/Nat/document/NatClass.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{NatClass}% +\isamarkupfalse% % \isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}% } diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/IsarOverview/Isar/document/Induction.tex --- a/doc-src/IsarOverview/Isar/document/Induction.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/IsarOverview/Isar/document/Induction.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Induction}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -120,7 +120,6 @@ natural number (remember: $0-1=0$):% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% \isacommand{lemma}\isamarkupfalse% \ {\isachardoublequoteopen}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline % @@ -653,7 +652,6 @@ The proof is so simple that it can be condensed to% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % @@ -675,7 +673,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/IsarOverview/Isar/document/Logic.tex --- a/doc-src/IsarOverview/Isar/document/Logic.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/IsarOverview/Isar/document/Logic.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Logic}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -1151,7 +1151,6 @@ \endisadelimML % \isatagML -\isamarkupfalse% % \endisatagML {\isafoldML}% @@ -1310,7 +1309,6 @@ \isamarkuptrue% % \renewcommand{\isamarkupcmt}[1]{#1} -\isamarkupfalse% % \isadelimproof % @@ -1320,8 +1318,7 @@ \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 @@ -1335,8 +1332,7 @@ } \isanewline \ \ \ \ \isacommand{have}\isamarkupfalse% -\ {\isacharquery}thesis\ \isamarkupfalse% -\ % +\ {\isacharquery}thesis\ \ % \isamarkupcmt{\dots% } \ \isacommand{{\isacharbraceright}}\isamarkupfalse% @@ -1351,8 +1347,7 @@ } \isanewline \ \ \ \ \isacommand{have}\isamarkupfalse% -\ {\isacharquery}thesis\ \isamarkupfalse% -\ % +\ {\isacharquery}thesis\ \ % \isamarkupcmt{\dots% } \ \isacommand{{\isacharbraceright}}\isamarkupfalse% @@ -1367,8 +1362,7 @@ } \isanewline \ \ \ \ \isacommand{have}\isamarkupfalse% -\ {\isacharquery}thesis\ \isamarkupfalse% -\ % +\ {\isacharquery}thesis\ \ % \isamarkupcmt{\dots% } \ \isacommand{{\isacharbraceright}}\isamarkupfalse% @@ -1450,7 +1444,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -1472,7 +1465,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -1541,8 +1533,7 @@ \ \ \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}% % @@ -1614,7 +1605,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/IsarOverview/Isar/document/isabelle.sty --- a/doc-src/IsarOverview/Isar/document/isabelle.sty Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/IsarOverview/Isar/document/isabelle.sty Mon Aug 29 11:44:23 2005 +0200 @@ -22,10 +22,10 @@ \newcommand{\isamath}[1]{\emph{$#1$}} \newcommand{\isatext}[1]{\emph{#1}} \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} -\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} @@ -89,6 +89,8 @@ \chardef\isacharbar=`\| \chardef\isacharbraceright=`\} \chardef\isachartilde=`\~ +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk} +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright} % keyword and section markup @@ -165,6 +167,8 @@ \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}% +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}% } \newcommand{\isabellestylesl}{% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/Locales/Locales/document/Locales.tex --- a/doc-src/Locales/Locales/document/Locales.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/Locales/Locales/document/Locales.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{Locales}% +\isamarkupfalse% % \isadelimtheory \isanewline @@ -8,7 +9,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -22,7 +22,6 @@ \endisadelimML % \isatagML -\isamarkupfalse% % \endisatagML {\isafoldML}% @@ -460,7 +459,6 @@ \endisadelimML % \isatagML -\isamarkupfalse% % \endisatagML {\isafoldML}% @@ -1309,7 +1307,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/Locales/Locales/document/isabelle.sty --- a/doc-src/Locales/Locales/document/isabelle.sty Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/Locales/Locales/document/isabelle.sty Mon Aug 29 11:44:23 2005 +0200 @@ -22,10 +22,10 @@ \newcommand{\isamath}[1]{\emph{$#1$}} \newcommand{\isatext}[1]{\emph{#1}} \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} -\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} @@ -89,6 +89,8 @@ \chardef\isacharbar=`\| \chardef\isacharbraceright=`\} \chardef\isachartilde=`\~ +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk} +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright} % keyword and section markup @@ -165,6 +167,8 @@ \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}% +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}% } \newcommand{\isabellestylesl}{% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Advanced/document/Partial.tex --- a/doc-src/TutorialI/Advanced/document/Partial.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Advanced/document/Partial.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Partial}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -339,7 +339,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Advanced/document/WFrec.tex --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{WFrec}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -150,8 +150,6 @@ crucial hint\cmmdx{hints} to our definition:% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}greater{\isacharparenright}% \begin{isamarkuptext}% \noindent @@ -169,7 +167,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Advanced/document/simp.tex --- a/doc-src/TutorialI/Advanced/document/simp.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{simp}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -236,7 +236,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/CTL/document/Base.tex --- a/doc-src/TutorialI/CTL/document/Base.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/CTL/document/Base.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Base}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -117,7 +117,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{CTL}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -29,7 +29,6 @@ \isa{formula} by a new constructor% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula% \begin{isamarkuptext}% \noindent @@ -51,8 +50,6 @@ a new datatype and a new function.}% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% {\isachardoublequoteopen}s\ {\isasymTurnstile}\ AF\ f\ \ \ \ {\isacharequal}\ {\isacharparenleft}{\isasymforall}p\ {\isasymin}\ Paths\ s{\isachardot}\ {\isasymexists}i{\isachardot}\ p\ i\ {\isasymTurnstile}\ f{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent @@ -69,8 +66,6 @@ \isa{mc\ f} and all states all of whose direct successors are in \isa{T}:% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% {\isachardoublequoteopen}mc{\isacharparenleft}AF\ f{\isacharparenright}\ \ \ \ {\isacharequal}\ lfp{\isacharparenleft}af{\isacharparenleft}mc\ f{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent @@ -98,15 +93,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -114,27 +106,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -392,28 +369,12 @@ where \isa{nat{\isacharunderscore}rec} is the predefined primitive recursor on \isa{nat}.% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -518,8 +479,7 @@ \isacommand{primrec}\isamarkupfalse% \isanewline {\isachardoublequoteopen}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline -{\isachardoublequoteopen}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequoteclose}\isamarkupfalse% -% +{\isachardoublequoteopen}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent Expressing the semantics of \isa{EU} is now straightforward: @@ -546,21 +506,12 @@ For more CTL exercises see, for example, Huth and Ryan \cite{Huth-Ryan-book}.% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -568,16 +519,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -585,24 +532,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -631,7 +566,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/CTL/document/CTLind.tex --- a/doc-src/TutorialI/CTL/document/CTLind.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{CTLind}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -137,8 +137,7 @@ \ \isacommand{apply}\isamarkupfalse% {\isacharparenleft}erule{\isacharunderscore}tac\ a\ {\isacharequal}\ t\ \isakeyword{in}\ wf{\isacharunderscore}induct{\isacharparenright}\isanewline \ \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}clarsimp{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}clarsimp{\isacharparenright}% \begin{isamarkuptxt}% \noindent \begin{isabelle}% @@ -239,7 +238,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/CTL/document/PDL.tex --- a/doc-src/TutorialI/CTL/document/PDL.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{PDL}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -145,8 +145,7 @@ \ \isacommand{apply}\isamarkupfalse% {\isacharparenleft}rule\ subsetI{\isacharparenright}\isanewline \ \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}simp{\isacharparenright}% \begin{isamarkuptxt}% \noindent Simplification leaves us with the following first subgoal @@ -293,16 +292,12 @@ \index{PDL|)}% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -310,15 +305,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -326,17 +318,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -350,7 +337,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{CodeGen}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -116,7 +116,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -145,7 +144,6 @@ instruction sequences:% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -171,8 +169,7 @@ \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -187,8 +184,6 @@ rewritten as% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % @@ -196,8 +191,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -216,14 +210,12 @@ \index{compiling expressions example|)}% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -237,7 +229,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Datatype/document/ABexpr.tex --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{ABexpr}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -130,8 +130,7 @@ \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}\isamarkupfalse% -\ simp{\isacharunderscore}all\isamarkupfalse% -% +\ simp{\isacharunderscore}all% \endisatagproof {\isafoldproof}% % @@ -161,18 +160,12 @@ \end{exercise}% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -180,18 +173,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -205,7 +192,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Fundata}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -72,14 +72,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% % \begin{isamarkuptxt}% \noindent @@ -92,7 +90,6 @@ \end{isabelle}% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -106,7 +103,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Nested}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -26,7 +26,6 @@ where function symbols can be applied to a list of arguments:% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% \isacommand{datatype}\isamarkupfalse% \ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequoteopen}term{\isachardoublequoteclose}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}% \begin{isamarkuptext}% @@ -140,16 +139,12 @@ that the suggested equation holds:% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -157,17 +152,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -175,15 +165,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -243,7 +230,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Datatype/document/unfoldnested.tex --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{unfoldnested}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -23,7 +23,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Documents}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -156,14 +156,12 @@ specifies an Isabelle symbol for the new operator:% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimML % \endisadelimML % \isatagML -\isamarkupfalse% % \endisatagML {\isafoldML}% @@ -174,8 +172,7 @@ \isacommand{constdefs}\isamarkupfalse% \isanewline \ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isanewline -\ \ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isamarkupfalse% -% +\ \ {\isachardoublequoteopen}A\ {\isasymoplus}\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}\ B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent The X-Symbol package within Proof~General provides several input methods to enter \isa{{\isasymoplus}} in the text. If all fails one may @@ -189,14 +186,12 @@ consider the following hybrid declaration of \isa{xor}:% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimML % \endisadelimML % \isatagML -\isamarkupfalse% % \endisatagML {\isafoldML}% @@ -211,8 +206,7 @@ \isanewline \isacommand{syntax}\isamarkupfalse% \ {\isacharparenleft}xsymbols{\isacharparenright}\isanewline -\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\isamarkupfalse% -% +\ \ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymoplus}{\isasymignore}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}% \begin{isamarkuptext}% The \commdx{syntax} command introduced here acts like \isakeyword{consts}, but without declaring a logical constant. The @@ -918,7 +912,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Ifexpr}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -180,7 +180,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -203,8 +202,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -212,15 +209,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -259,8 +253,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -268,15 +260,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -303,21 +292,12 @@ \index{boolean expressions example|)}% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -325,15 +305,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -341,15 +318,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -357,15 +331,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -379,7 +350,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{AB}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -309,8 +309,7 @@ \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}induct{\isacharunderscore}tac\ w\ rule{\isacharcolon}\ length{\isacharunderscore}induct{\isacharparenright}% \begin{isamarkuptxt}% \noindent The \isa{rule} parameter tells \isa{induct{\isacharunderscore}tac} explicitly which induction @@ -325,8 +324,7 @@ \isacommand{apply}\isamarkupfalse% {\isacharparenleft}case{\isacharunderscore}tac\ w{\isacharparenright}\isanewline \ \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}simp{\isacharunderscore}all{\isacharparenright}% \begin{isamarkuptxt}% \noindent Simplification disposes of the base case and leaves only a conjunction @@ -452,7 +450,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{Advanced}% +\isamarkupfalse% % \isadelimtheory \isanewline diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{Even}% +\isamarkupfalse% % \isadelimtheory \isanewline diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Inductive/document/Mutual.tex --- a/doc-src/TutorialI/Inductive/document/Mutual.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Mutual}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -80,13 +80,6 @@ We do not show the proof script.% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -100,7 +93,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Inductive/document/Star.tex --- a/doc-src/TutorialI/Inductive/document/Star.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Star}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -135,7 +135,6 @@ transfer the additional premise \isa{{\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}} into the conclusion:% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -283,17 +282,12 @@ \end{exercise}% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -307,7 +301,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/AdvancedInd.tex --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{AdvancedInd}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -82,7 +82,6 @@ result to the usual \isa{{\isasymLongrightarrow}} form:% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -97,7 +96,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \begin{isamarkuptxt}% \noindent @@ -155,7 +153,6 @@ the notation $\overline{y}$ is merely an informal device.% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -303,7 +300,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -432,7 +428,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Itrev}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -111,7 +111,6 @@ just not true. The correct generalization is% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -126,7 +125,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \begin{isamarkuptxt}% \noindent @@ -151,7 +149,6 @@ for all \isa{ys} instead of a fixed one:% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -166,7 +163,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -216,7 +212,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/Option2.tex --- a/doc-src/TutorialI/Misc/document/Option2.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/Option2.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Option{\isadigit{2}}}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -15,8 +15,6 @@ \isadelimtheory % \endisadelimtheory -\isamarkupfalse% -\isamarkupfalse% % \begin{isamarkuptext}% \indexbold{*option (type)}\indexbold{*None (constant)}% @@ -45,7 +43,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/Plus.tex --- a/doc-src/TutorialI/Misc/document/Plus.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/Plus.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Plus}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -30,15 +30,12 @@ \noindent and prove% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -53,7 +50,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -67,7 +63,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/Tree.tex --- a/doc-src/TutorialI/Misc/document/Tree.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Tree}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -22,9 +22,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{datatype}\isamarkupfalse% -\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\isamarkupfalse% -\isamarkupfalse% -% +\ {\isacharprime}a\ tree\ {\isacharequal}\ Tip\ {\isacharbar}\ Node\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}\ {\isacharprime}a\ {\isachardoublequoteopen}{\isacharprime}a\ tree{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent Define a function \isa{mirror} that mirrors a binary tree @@ -38,8 +36,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -47,8 +43,6 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% -\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -63,8 +57,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -78,7 +70,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/Tree2.tex --- a/doc-src/TutorialI/Misc/document/Tree2.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Tree{\isadigit{2}}}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -25,21 +25,17 @@ \end{isamarkuptext}% \isamarkuptrue% \isacommand{consts}\isamarkupfalse% -\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isamarkupfalse% -% +\ flatten{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent Define \isa{flatten{\isadigit{2}}} and prove% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -54,7 +50,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -68,7 +63,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/appendix.tex --- a/doc-src/TutorialI/Misc/document/appendix.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/appendix.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{appendix}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -53,7 +53,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/case_exprs.tex --- a/doc-src/TutorialI/Misc/document/case_exprs.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/case_exprs.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{case{\isacharunderscore}exprs}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -100,8 +100,7 @@ \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}auto{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}auto{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -135,7 +134,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/fakenat.tex --- a/doc-src/TutorialI/Misc/document/fakenat.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{fakenat}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -29,7 +29,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/natsum.tex --- a/doc-src/TutorialI/Misc/document/natsum.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{natsum}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -118,7 +118,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -141,7 +140,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -169,8 +167,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}arith{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}arith{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -190,7 +187,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -224,7 +220,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/pairs.tex --- a/doc-src/TutorialI/Misc/document/pairs.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{pairs}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -52,7 +52,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/prime_def.tex --- a/doc-src/TutorialI/Misc/document/prime_def.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{prime{\isacharunderscore}def}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -15,7 +15,6 @@ \isadelimtheory % \endisadelimtheory -\isamarkupfalse% % \begin{isamarkuptext}% \begin{warn} @@ -41,7 +40,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/simp.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{simp}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -261,7 +261,6 @@ can be proved by simplification. Thus we could have proved the lemma outright by% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -269,7 +268,6 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % @@ -277,8 +275,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}simp\ add{\isacharcolon}\ xor{\isacharunderscore}def{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -390,7 +387,6 @@ \endisadelimproof % \isatagproof -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -450,7 +446,6 @@ Let us simplify a case analysis over lists:\index{*list.split (theorem)}% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -482,7 +477,6 @@ lemma above can be proved in one step by% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -490,7 +484,6 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % @@ -498,8 +491,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}simp\ split{\isacharcolon}\ list{\isachardot}split{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -524,7 +516,6 @@ either locally% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % @@ -532,8 +523,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}simp\ split\ del{\isacharcolon}\ split{\isacharunderscore}if{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -594,7 +584,6 @@ \end{warn}% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -622,8 +611,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}simp{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}simp{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -772,7 +760,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Misc/document/types.tex --- a/doc-src/TutorialI/Misc/document/types.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Misc/document/types.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{types}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -76,7 +76,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Recdef/document/Induction.tex --- a/doc-src/TutorialI/Recdef/document/Induction.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Induction}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -108,7 +108,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Recdef/document/Nested0.tex --- a/doc-src/TutorialI/Recdef/document/Nested0.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested0.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Nested{\isadigit{0}}}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -42,7 +42,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Recdef/document/Nested1.tex --- a/doc-src/TutorialI/Recdef/document/Nested1.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Nested{\isadigit{1}}}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -62,7 +62,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Recdef/document/Nested2.tex --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Nested{\isadigit{2}}}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -32,7 +32,6 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -116,8 +115,6 @@ the recursion equations:\cmmdx{hints}% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}% \begin{isamarkuptext}% \noindent @@ -142,7 +139,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Recdef/document/examples.tex --- a/doc-src/TutorialI/Recdef/document/examples.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{examples}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -120,7 +120,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Recdef/document/simplification.tex --- a/doc-src/TutorialI/Recdef/document/simplification.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{simplification}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -158,7 +158,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{termination}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -60,14 +60,11 @@ simplification rule.\cmmdx{hints}% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% \isacommand{recdef}\isamarkupfalse% \ qs\ {\isachardoublequoteopen}measure\ length{\isachardoublequoteclose}\isanewline \ {\isachardoublequoteopen}qs\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline \ {\isachardoublequoteopen}qs{\isacharparenleft}x{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ y{\isasymle}x{\isacharparenright}\ xs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharat}\ qs{\isacharparenleft}filter\ {\isacharparenleft}{\isasymlambda}y{\isachardot}\ x{\isacharless}y{\isacharparenright}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline -{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le{\isacharparenright}% \begin{isamarkuptext}% \noindent This time everything works fine. Now \isa{qs{\isachardot}simps} contains precisely @@ -111,7 +108,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Rules/document/find2.tex --- a/doc-src/TutorialI/Rules/document/find2.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Rules/document/find2.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{find{\isadigit{2}}}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -15,7 +15,6 @@ \isadelimtheory % \endisadelimtheory -\isamarkupfalse% % \isadelimproof % @@ -42,7 +41,6 @@ database. Given the goal% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -50,7 +48,6 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % @@ -78,7 +75,6 @@ into account, too.% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -92,7 +88,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{ToyList}% +\isamarkupfalse% % \isadelimtheory % @@ -248,7 +249,6 @@ In order to simplify this subgoal further, a lemma suggests itself.% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -304,7 +304,6 @@ embarking on the proof of a lemma usually remains implicit.% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -398,7 +397,6 @@ and the missing lemma is associativity of \isa{{\isacharat}}.% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Trie}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -218,18 +218,12 @@ \end{exercise}% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -237,18 +231,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -256,18 +244,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -275,22 +257,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -298,18 +270,12 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \isadelimproof % \endisadelimproof % \isatagproof -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -323,7 +289,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Axioms.tex --- a/doc-src/TutorialI/Types/document/Axioms.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Axioms}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -374,7 +374,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{Numbers}% +\isamarkupfalse% % \isadelimtheory \isanewline @@ -560,7 +561,7 @@ % \isatagML \isacommand{ML}\isamarkupfalse% -{\isacharbraceleft}{\isacharasterisk}set\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}% +{\isacharverbatimopen}set\ show{\isacharunderscore}sorts{\isacharverbatimclose}% \endisatagML {\isafoldML}% % @@ -585,7 +586,7 @@ % \isatagML \isacommand{ML}\isamarkupfalse% -{\isacharbraceleft}{\isacharasterisk}reset\ show{\isacharunderscore}sorts{\isacharasterisk}{\isacharbraceright}% +{\isacharverbatimopen}reset\ show{\isacharunderscore}sorts{\isacharverbatimclose}% \endisatagML {\isafoldML}% % diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Overloading.tex --- a/doc-src/TutorialI/Types/document/Overloading.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Overloading}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -53,7 +53,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Overloading0.tex --- a/doc-src/TutorialI/Types/document/Overloading0.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading0.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Overloading{\isadigit{0}}}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -68,7 +68,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Overloading1.tex --- a/doc-src/TutorialI/Types/document/Overloading1.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading1.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Overloading{\isadigit{1}}}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -126,7 +126,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Overloading2.tex --- a/doc-src/TutorialI/Types/document/Overloading2.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Overloading{\isadigit{2}}}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -83,7 +83,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Pairs.tex --- a/doc-src/TutorialI/Types/document/Pairs.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Pairs}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -132,7 +132,6 @@ simplification and splitting in one command that proves the goal outright:% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -140,7 +139,6 @@ \isadelimproof % \endisadelimproof -\isamarkupfalse% % \isadelimproof % @@ -178,7 +176,6 @@ can be split as above. The same is true for paired set comprehension:% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -206,7 +203,6 @@ The same proof procedure works for% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -231,7 +227,6 @@ may be present in the goal. Consider the following function:% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -285,7 +280,6 @@ with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:% \end{isamarkuptxt}% \isamarkuptrue% -\isamarkupfalse% % \endisatagproof {\isafoldproof}% @@ -335,7 +329,6 @@ where two separate \isa{simp} applications succeed.% \end{isamarkuptext}% \isamarkuptrue% -\isamarkupfalse% % \isadelimproof % @@ -343,8 +336,7 @@ % \isatagproof \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% -% +{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}% \endisatagproof {\isafoldproof}% % @@ -395,7 +387,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Records.tex --- a/doc-src/TutorialI/Types/document/Records.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Types/document/Records.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,6 +1,7 @@ % \begin{isabellebody}% \def\isabellecontext{Records}% +\isamarkupfalse% % \isamarkupheader{Records \label{sec:records}% } @@ -11,7 +12,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -653,7 +653,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/Types/document/Typedefs.tex --- a/doc-src/TutorialI/Types/document/Typedefs.tex Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/Types/document/Typedefs.tex Mon Aug 29 11:44:23 2005 +0200 @@ -1,13 +1,13 @@ % \begin{isabellebody}% \def\isabellecontext{Typedefs}% +\isamarkupfalse% % \isadelimtheory % \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% @@ -329,7 +329,6 @@ \endisadelimtheory % \isatagtheory -\isamarkupfalse% % \endisatagtheory {\isafoldtheory}% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/TutorialI/isabelle.sty --- a/doc-src/TutorialI/isabelle.sty Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/TutorialI/isabelle.sty Mon Aug 29 11:44:23 2005 +0200 @@ -22,10 +22,10 @@ \newcommand{\isamath}[1]{\emph{$#1$}} \newcommand{\isatext}[1]{\emph{#1}} \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} -\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} @@ -89,6 +89,8 @@ \chardef\isacharbar=`\| \chardef\isacharbraceright=`\} \chardef\isachartilde=`\~ +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk} +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright} % keyword and section markup @@ -165,6 +167,8 @@ \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}% +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}% } \newcommand{\isabellestylesl}{% diff -r 5fefe658a6f8 -r 5f42dd5e6570 doc-src/ZF/isabelle.sty --- a/doc-src/ZF/isabelle.sty Mon Aug 29 10:28:17 2005 +0200 +++ b/doc-src/ZF/isabelle.sty Mon Aug 29 11:44:23 2005 +0200 @@ -22,10 +22,10 @@ \newcommand{\isamath}[1]{\emph{$#1$}} \newcommand{\isatext}[1]{\emph{#1}} \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} -\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}} -\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}} +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} @@ -89,6 +89,8 @@ \chardef\isacharbar=`\| \chardef\isacharbraceright=`\} \chardef\isachartilde=`\~ +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk} +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright} % keyword and section markup @@ -165,6 +167,8 @@ \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% +\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}% +\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}% } \newcommand{\isabellestylesl}{%