equal
deleted
inserted
replaced
60 (Attrib.empty_binding, eq) |
60 (Attrib.empty_binding, eq) |
61 end |
61 end |
62 *} |
62 *} |
63 |
63 |
64 ML {* |
64 ML {* |
|
65 (* proves the two pt-type class properties *) |
65 fun prove_permute_zero lthy induct perm_defs perm_fns = |
66 fun prove_permute_zero lthy induct perm_defs perm_fns = |
66 let |
67 let |
67 val perm_types = map (body_type o fastype_of) perm_fns |
68 val perm_types = map (body_type o fastype_of) perm_fns |
68 val perm_indnames = Datatype_Prop.make_tnames perm_types |
69 val perm_indnames = Datatype_Prop.make_tnames perm_types |
69 |
70 |