equal
deleted
inserted
replaced
314 |
314 |
315 val ((_, (_ , def_thm)), lthy') = |
315 val ((_, (_ , def_thm)), lthy') = |
316 Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy |
316 Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy |
317 |
317 |
318 val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}) |
318 val transfer_thm = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}) |
319 |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy') |
319 |> Raw_Simplifier.rewrite_rule (Transfer.get_sym_relator_eq lthy') |
320 |
320 |
321 val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm |
321 val abs_eq_thm = generate_abs_eq lthy' def_thm rsp_thm quot_thm |
322 val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty) |
322 val maybe_rep_eq_thm = generate_rep_eq lthy' def_thm rsp_thm (rty_forced, qty) |
323 |
323 |
324 fun qualify defname suffix = Binding.qualified true suffix defname |
324 fun qualify defname suffix = Binding.qualified true suffix defname |