| author | nipkow |
| Thu, 29 May 2008 22:45:33 +0200 | |
| changeset 27015 | f8537d69f514 |
| parent 26729 | 43a72d892594 |
| child 38430 | 254a021ed66e |
| permissions | -rw-r--r-- |
| 15136 | 1 |
theory ToyList |
| 26729 | 2 |
imports Datatype |
| 15136 | 3 |
begin |
| 8751 | 4 |
|
5 |
datatype 'a list = Nil ("[]")
|
|
| 9541 | 6 |
| Cons 'a "'a list" (infixr "#" 65) |
| 8751 | 7 |
|
| 27015 | 8 |
primrec app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
9 |
where |
|
10 |
"[] @ ys = ys" | |
|
| 9541 | 11 |
"(x # xs) @ ys = x # (xs @ ys)" |
| 8751 | 12 |
|
| 27015 | 13 |
primrec rev :: "'a list => 'a list" where |
14 |
"rev [] = []" | |
|
| 9541 | 15 |
"rev (x # xs) = (rev xs) @ (x # [])" |