equal
deleted
inserted
replaced
26 type_intrs "[list_univ RS subsetD]" |
26 type_intrs "[list_univ RS subsetD]" |
27 *) |
27 *) |
28 |
28 |
29 defs |
29 defs |
30 term_rec_def |
30 term_rec_def |
31 "term_rec(t,d) == \ |
31 "term_rec(t,d) == |
32 \ Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))" |
32 Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))" |
33 |
33 |
34 term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))" |
34 term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))" |
35 |
35 |
36 term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))" |
36 term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))" |
37 |
37 |