equal
deleted
inserted
replaced
97 \noindent From now on, terms like \isa{Suc\ {\isacharparenleft}m\ {\isasymoplus}\ {\isadigit{2}}{\isacharparenright}} are |
97 \noindent From now on, terms like \isa{Suc\ {\isacharparenleft}m\ {\isasymoplus}\ {\isadigit{2}}{\isacharparenright}} are |
98 legal.% |
98 legal.% |
99 \end{isamarkuptext}% |
99 \end{isamarkuptext}% |
100 \isamarkuptrue% |
100 \isamarkuptrue% |
101 \isacommand{instantiation}\isamarkupfalse% |
101 \isacommand{instantiation}\isamarkupfalse% |
102 \ {\isachardoublequoteopen}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline |
102 \ prod\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}plus{\isacharcomma}\ plus{\isacharparenright}\ plus\isanewline |
103 \isakeyword{begin}% |
103 \isakeyword{begin}% |
104 \begin{isamarkuptext}% |
104 \begin{isamarkuptext}% |
105 \noindent Here we instantiate the product type \isa{{\isacharasterisk}} to |
105 \noindent Here we instantiate the product type \isa{prod} to |
106 class \isa{plus}, given that its type arguments are of |
106 class \isa{plus}, given that its type arguments are of |
107 class \isa{plus}:% |
107 class \isa{plus}:% |
108 \end{isamarkuptext}% |
108 \end{isamarkuptext}% |
109 \isamarkuptrue% |
109 \isamarkuptrue% |
110 \isacommand{fun}\isamarkupfalse% |
110 \isacommand{fun}\isamarkupfalse% |