equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Nested1}% |
3 \def\isabellecontext{Nested1}% |
4 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}% |
4 % |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 \noindent |
6 \noindent |
7 Although the definition of \isa{trev} is quite natural, we will have |
7 Although the definition of \isa{trev} is quite natural, we will have |
8 overcome a minor difficulty in convincing Isabelle of is termination. |
8 overcome a minor difficulty in convincing Isabelle of is termination. |
9 It is precisely this difficulty that is the \textit{raison d'\^etre} of |
9 It is precisely this difficulty that is the \textit{raison d'\^etre} of |