equal
deleted
inserted
replaced
6 header {* The datatype of finite lists *} |
6 header {* The datatype of finite lists *} |
7 |
7 |
8 theory List |
8 theory List |
9 imports PreList |
9 imports PreList |
10 uses "Tools/string_syntax.ML" |
10 uses "Tools/string_syntax.ML" |
|
11 ("Tools/function_package/lexicographic_order.ML") |
|
12 ("Tools/function_package/fundef_datatype.ML") |
11 begin |
13 begin |
12 |
14 |
13 datatype 'a list = |
15 datatype 'a list = |
14 Nil ("[]") |
16 Nil ("[]") |
15 | Cons 'a "'a list" (infixr "#" 65) |
17 | Cons 'a "'a list" (infixr "#" 65) |