changeset 15140 | 322485b816ac |
parent 15131 | c69542757a4d |
child 15168 | 33a08cfc3ae5 |
15139:58cd3404cf75 | 15140:322485b816ac |
---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* The datatype of finite lists *} |
6 header {* The datatype of finite lists *} |
7 |
7 |
8 theory List |
8 theory List |
9 import PreList |
9 imports PreList |
10 begin |
10 begin |
11 |
11 |
12 datatype 'a list = |
12 datatype 'a list = |
13 Nil ("[]") |
13 Nil ("[]") |
14 | Cons 'a "'a list" (infixr "#" 65) |
14 | Cons 'a "'a list" (infixr "#" 65) |