equal
deleted
inserted
replaced
337 using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto |
337 using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto |
338 |
338 |
339 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs" |
339 lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs" |
340 using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp |
340 using 1 2 unfolding Quotient_alt_def reflp_def fun_rel_def by simp |
341 |
341 |
|
342 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x" |
|
343 using 1 2 assms unfolding Quotient_alt_def reflp_def by metis |
|
344 |
342 end |
345 end |
343 |
346 |
344 text {* Generating transfer rules for a type defined with @{text "typedef"}. *} |
347 text {* Generating transfer rules for a type defined with @{text "typedef"}. *} |
345 |
348 |
346 context |
349 context |