| changeset 15136 | 1275417e3930 |
| parent 9541 | d17c0b34d5c8 |
| child 15141 | a95c2ff210ba |
| 15135:f00857c7539b | 15136:1275417e3930 |
|---|---|
1 theory ToyList = PreList: |
1 theory ToyList |
2 import PreList |
|
3 begin |
|
2 |
4 |
3 datatype 'a list = Nil ("[]") |
5 datatype 'a list = Nil ("[]") |
4 | Cons 'a "'a list" (infixr "#" 65) |
6 | Cons 'a "'a list" (infixr "#" 65) |
5 |
7 |
6 consts app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
8 consts app :: "'a list => 'a list => 'a list" (infixr "@" 65) |