equal
deleted
inserted
replaced
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 = Datatype + WF_Rel + NatBin + |
9 List = PreList + |
10 |
10 |
11 datatype 'a list = Nil ("[]") | Cons 'a ('a list) (infixr "#" 65) |
11 datatype 'a list = Nil ("[]") | Cons '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) |