equal
deleted
inserted
replaced
69 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
69 fun typedef_make (vs, qty_name, mx, rel, rty) lthy = |
70 let |
70 let |
71 val typedef_tac = |
71 val typedef_tac = |
72 EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) |
72 EVERY1 (map rtac [@{thm exI}, mem_def2, @{thm exI}, @{thm refl}]) |
73 in |
73 in |
74 Local_Theory.theory_result |
74 Typedef.add_typedef false NONE |
75 (Typedef.add_typedef false NONE |
|
76 (qty_name, vs, mx) |
75 (qty_name, vs, mx) |
77 (typedef_term rel rty lthy) |
76 (typedef_term rel rty lthy) |
78 NONE typedef_tac) lthy |
77 NONE typedef_tac lthy |
79 end |
78 end |
80 |
79 |
81 |
80 |
82 (* tactic to prove the quot_type theorem for the new type *) |
81 (* tactic to prove the quot_type theorem for the new type *) |
83 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |
82 fun typedef_quot_type_tac equiv_thm (typedef_info: Typedef.info) = |