equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory natsum = Main:; |
2 theory natsum = Main:; |
3 (*>*) |
3 (*>*) |
4 text{*\noindent |
4 text{*\noindent |
5 In particular, there are \isa{case}-expressions, for example |
5 In particular, there are @{text"case"}-expressions, for example |
6 \begin{quote} |
6 \begin{quote} |
7 @{term[display]"case n of 0 => 0 | Suc m => m"} |
7 @{term[display]"case n of 0 => 0 | Suc m => m"} |
8 \end{quote} |
8 \end{quote} |
9 primitive recursion, for example |
9 primitive recursion, for example |
10 *} |
10 *} |