equal
deleted
inserted
replaced
181 |
181 |
182 val ((_, (_ , def_thm)), lthy') = |
182 val ((_, (_ , def_thm)), lthy') = |
183 Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy |
183 Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy |
184 |
184 |
185 val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer} |
185 val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer} |
|
186 |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy') |
186 |
187 |
187 fun qualify defname suffix = Binding.name suffix |
188 fun qualify defname suffix = Binding.name suffix |
188 |> Binding.qualify true defname |
189 |> Binding.qualify true defname |
189 |
190 |
190 val lhs_name = Binding.name_of (#1 var) |
191 val lhs_name = Binding.name_of (#1 var) |