| author | haftmann |
| Tue, 26 Feb 2008 20:38:12 +0100 | |
| changeset 26147 | ae2bf929e33c |
| parent 15141 | a95c2ff210ba |
| child 26729 | 43a72d892594 |
| permissions | -rw-r--r-- |
| 15136 | 1 |
theory ToyList |
| 15141 | 2 |
imports PreList |
| 15136 | 3 |
begin |
| 8751 | 4 |
|
5 |
datatype 'a list = Nil ("[]")
|
|
| 9541 | 6 |
| Cons 'a "'a list" (infixr "#" 65) |
| 8751 | 7 |
|
8 |
consts app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
|
| 9541 | 9 |
rev :: "'a list => 'a list" |
| 8751 | 10 |
|
11 |
primrec |
|
12 |
"[] @ ys = ys" |
|
| 9541 | 13 |
"(x # xs) @ ys = x # (xs @ ys)" |
| 8751 | 14 |
|
15 |
primrec |
|
16 |
"rev [] = []" |
|
| 9541 | 17 |
"rev (x # xs) = (rev xs) @ (x # [])" |