src/HOL/Quotient.thy
changeset 47361 87c0eaf04bad
parent 47308 9caab698dbe4
child 47362 b1f099bdfbba
     1.1 --- a/src/HOL/Quotient.thy	Wed Apr 04 16:29:17 2012 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Wed Apr 04 17:51:12 2012 +0200
     1.3 @@ -772,24 +772,6 @@
     1.4  using assms
     1.5  by (rule OOO_quotient3) auto
     1.6  
     1.7 -subsection {* Invariant *}
     1.8 -
     1.9 -lemma copy_type_to_Quotient3:
    1.10 -  assumes "type_definition Rep Abs UNIV"
    1.11 -  shows "Quotient3 (op =) Abs Rep"
    1.12 -proof -
    1.13 -  interpret type_definition Rep Abs UNIV by fact
    1.14 -  from Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I)
    1.15 -qed
    1.16 -
    1.17 -lemma invariant_type_to_Quotient3:
    1.18 -  assumes "type_definition Rep Abs {x. P x}"
    1.19 -  shows "Quotient3 (Lifting.invariant P) Abs Rep"
    1.20 -proof -
    1.21 -  interpret type_definition Rep Abs "{x. P x}" by fact
    1.22 -  from Rep Abs_inject Rep_inverse show ?thesis by (auto intro!: Quotient3I simp: invariant_def)
    1.23 -qed
    1.24 -
    1.25  subsection {* ML setup *}
    1.26  
    1.27  text {* Auxiliary data for the quotient package *}