| changeset 352 | fd3ab8bcb69d |
| parent 0 | a5a9c433f639 |
| child 1322 | 9b3d3362a048 |
| 351:1718ce07a584 | 352:fd3ab8bcb69d |
|---|---|
6 Examples of simplification and induction on lists |
6 Examples of simplification and induction on lists |
7 *) |
7 *) |
8 |
8 |
9 List = Nat2 + |
9 List = Nat2 + |
10 |
10 |
11 types list 1 |
11 types 'a list |
12 arities list :: (term)term |
12 arities list :: (term)term |
13 |
13 |
14 consts |
14 consts |
15 hd :: "'a list => 'a" |
15 hd :: "'a list => 'a" |
16 tl :: "'a list => 'a list" |
16 tl :: "'a list => 'a list" |