135   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp

   135   then show "R (REP a) (REP b) \<equiv> (a = b)" by simp

   136 qed

   136 qed

   137 

   137 

   138 end

   138 end

   139 

   139 

   141 section {* type definition for the quotient type *}

   140 section {* type definition for the quotient type *}

   142 

   141 

   143 (* the auxiliary data for the quotient types *)

   142 (* the auxiliary data for the quotient types *)

   144 use "quotient_info.ML"

   143 use "quotient_info.ML"

   145 

   144 

   157 use "quotient.ML"

   156 use "quotient.ML"

   158 

   157 

   159 

   158 

   160 (* lifting of constants *)

   159 (* lifting of constants *)

   161 use "quotient_def.ML"

   160 use "quotient_def.ML"

   162 

   163 

   163 section {* ATOMIZE *}

   164 section {* ATOMIZE *}

   164 

   165 

   165 lemma atomize_eqv[atomize]: 

   166 lemma atomize_eqv[atomize]: 

   166   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 

   167   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"