| changeset 4643 | 1b40fcac5a09 |
| parent 4605 | 579e0ef2df6b |
| child 5077 | 71043526295f |
| 4642:2d3910d6ab10 | 4643:1b40fcac5a09 |
|---|---|
4 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
5 |
5 |
6 The datatype of finite lists. |
6 The datatype of finite lists. |
7 *) |
7 *) |
8 |
8 |
9 List = Divides + |
9 List = WF_Rel + |
10 |
10 |
11 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65) |
11 datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65) |
12 |
12 |
13 consts |
13 consts |
14 "@" :: ['a list, 'a list] => 'a list (infixr 65) |
14 "@" :: ['a list, 'a list] => 'a list (infixr 65) |