154 (* name equivalence theorem *) |
154 (* name equivalence theorem *) |
155 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
155 val equiv_thm_name = Binding.suffix_name "_equivp" qty_name |
156 |
156 |
157 (* storing the quot-info *) |
157 (* storing the quot-info *) |
158 val lthy4 = quotdata_update qty_full_name |
158 val lthy4 = quotdata_update qty_full_name |
159 (Logic.varifyT Abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy3 |
159 (Logic.varifyT Abs_ty, Logic.varifyT rty, map_types Logic.varifyT rel, equiv_thm) lthy3 |
160 (* FIXME: varifyT should not be used *) |
160 (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *) |
161 (* FIXME: the relation can be any term, that later maybe needs to be given *) |
161 (* FIXME: The relation can be any term, that later maybe needs to be given *) |
162 (* FIXME: a different type (in regularize_trm); how should this be done? *) |
162 (* FIXME: a different type (in regularize_trm); how should this be done? *) |
163 in |
163 in |
164 lthy4 |
164 lthy4 |
165 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
165 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
166 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
166 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |