changeset 8846 | c7d945398677 |
parent 8751 | 9ed0548177fb |
child 9541 | d17c0b34d5c8 |
8845:03a2ae3059da | 8846:c7d945398677 |
---|---|
1 theory ToyList = PreList: |
1 theory ToyList = PreList:; |
2 |
2 |
3 datatype 'a list = Nil ("[]") |
3 datatype 'a list = Nil ("[]") |
4 | Cons 'a "'a list" (infixr "#" 65); |
4 | Cons 'a "'a list" (infixr "#" 65); |
5 |
5 |
6 consts app :: "'a list => 'a list => 'a list" (infixr "@" 65) |
6 consts app :: "'a list => 'a list => 'a list" (infixr "@" 65) |