equal
deleted
inserted
replaced
43 fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy = |
43 fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy = |
44 let |
44 let |
45 val typedef_tac = |
45 val typedef_tac = |
46 EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) |
46 EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm]) |
47 in |
47 in |
48 Typedef.add_typedef false NONE (qty_name, map (rpair dummyS) vs, mx) |
48 Typedef.add_typedef NONE (qty_name, map (rpair dummyS) vs, mx) |
49 (typedef_term rel rty lthy) NONE typedef_tac lthy |
49 (typedef_term rel rty lthy) NONE typedef_tac lthy |
50 end |
50 end |
51 |
51 |
52 |
52 |
53 (* tactic to prove the quot_type theorem for the new type *) |
53 (* tactic to prove the quot_type theorem for the new type *) |