equal
deleted
inserted
replaced
8 map is a binding operator -- it applies to meta-level functions, not |
8 map is a binding operator -- it applies to meta-level functions, not |
9 object-level functions. This simplifies the final form of term_rec_conv, |
9 object-level functions. This simplifies the final form of term_rec_conv, |
10 although complicating its derivation. |
10 although complicating its derivation. |
11 *) |
11 *) |
12 |
12 |
13 List = Datatype + Arith + |
13 List = Datatype + ArithSimp + |
14 |
14 |
15 consts |
15 consts |
16 list :: i=>i |
16 list :: i=>i |
17 |
17 |
18 datatype |
18 datatype |