equal
deleted
inserted
replaced
4 % |
4 % |
5 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
6 \noindent |
6 \noindent |
7 In particular, there are \isa{case}-expressions, for example |
7 In particular, there are \isa{case}-expressions, for example |
8 \begin{isabelle}% |
8 \begin{isabelle}% |
9 \ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m% |
9 \ \ \ \ \ case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m% |
10 \end{isabelle} |
10 \end{isabelle} |
11 primitive recursion, for example% |
11 primitive recursion, for example% |
12 \end{isamarkuptext}% |
12 \end{isamarkuptext}% |
13 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
13 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
14 \isacommand{primrec}\ {\isachardoublequote}sum\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline |
14 \isacommand{primrec}\ {\isachardoublequote}sum\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline |
15 \ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}% |
15 \ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}% |
16 \begin{isamarkuptext}% |
16 \begin{isamarkuptext}% |
17 \noindent |
17 \noindent |
18 and induction, for example% |
18 and induction, for example% |
19 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |