153 |
153 |
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 |
|
159 (Logic.varifyT Abs_ty, Logic.varifyT rty, map_types Logic.varifyT rel, equiv_thm) lthy3 |
|
160 (* FIXME: VarifyT should not be used - at the moment it allows matching against the types. *) |
158 (* 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 *) |
159 fun qinfo phi = quotdata_transfer phi |
162 (* FIXME: a different type (in regularize_trm); how should this be done? *) |
160 {qtyp = Logic.varifyT Abs_ty, rtyp = Logic.varifyT rty, |
|
161 equiv_rel = map_types Logic.varifyT rel, equiv_thm = equiv_thm} |
|
162 val lthy4 = Local_Theory.declaration true |
|
163 (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 |
163 in |
164 in |
164 lthy4 |
165 lthy4 |
165 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
166 |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) |
166 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
167 ||>> note (equiv_thm_name, equiv_thm, [intern_attr equiv_rules_add]) |
167 end |
168 end |