equal
deleted
inserted
replaced
18 \begin{isamarkuptext}% |
18 \begin{isamarkuptext}% |
19 \noindent Define the following addition function% |
19 \noindent Define the following addition function% |
20 \end{isamarkuptext}% |
20 \end{isamarkuptext}% |
21 \isamarkuptrue% |
21 \isamarkuptrue% |
22 \isacommand{consts}\isamarkupfalse% |
22 \isacommand{consts}\isamarkupfalse% |
23 \ plus\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
23 \ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
24 \isacommand{primrec}\isamarkupfalse% |
24 \isacommand{primrec}\isamarkupfalse% |
25 \isanewline |
25 \isanewline |
26 {\isachardoublequoteopen}plus\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline |
26 {\isachardoublequoteopen}add\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline |
27 {\isachardoublequoteopen}plus\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ plus\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}% |
27 {\isachardoublequoteopen}add\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ add\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}% |
28 \begin{isamarkuptext}% |
28 \begin{isamarkuptext}% |
29 \noindent and prove% |
29 \noindent and prove% |
30 \end{isamarkuptext}% |
30 \end{isamarkuptext}% |
31 \isamarkuptrue% |
31 \isamarkuptrue% |
32 % |
32 % |
41 % |
41 % |
42 \isadelimproof |
42 \isadelimproof |
43 % |
43 % |
44 \endisadelimproof |
44 \endisadelimproof |
45 \isacommand{lemma}\isamarkupfalse% |
45 \isacommand{lemma}\isamarkupfalse% |
46 \ {\isachardoublequoteopen}plus\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequoteclose}% |
46 \ {\isachardoublequoteopen}add\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequoteclose}% |
47 \isadelimproof |
47 \isadelimproof |
48 % |
48 % |
49 \endisadelimproof |
49 \endisadelimproof |
50 % |
50 % |
51 \isatagproof |
51 \isatagproof |