| changeset 16417 | 9bc16273c2d4 |
| parent 15364 | 0c3891c3528f |
| child 16523 | f8a734dc0fbc |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory natsum = Main:; |
2 theory natsum imports Main begin; |
3 (*>*) |
3 (*>*) |
4 text{*\noindent |
4 text{*\noindent |
5 In particular, there are @{text"case"}-expressions, for example |
5 In particular, there are @{text"case"}-expressions, for example |
6 @{term[display]"case n of 0 => 0 | Suc m => m"} |
6 @{term[display]"case n of 0 => 0 | Suc m => m"} |
7 primitive recursion, for example |
7 primitive recursion, for example |