src/HOL/Quotient.thy
changeset 56073 29e308b56d23
parent 55945 e96383acecf9
child 57960 ee1ba4848896
     1.1 --- a/src/HOL/Quotient.thy	Wed Mar 12 22:57:50 2014 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Thu Mar 13 07:07:07 2014 +0100
     1.3 @@ -487,15 +487,7 @@
     1.4  
     1.5  lemma bex1_bexeq_reg:
     1.6    shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
     1.7 -  apply (simp add: Ex1_def Bex1_rel_def in_respects)
     1.8 -  apply clarify
     1.9 -  apply auto
    1.10 -  apply (rule bexI)
    1.11 -  apply assumption
    1.12 -  apply (simp add: in_respects)
    1.13 -  apply (simp add: in_respects)
    1.14 -  apply auto
    1.15 -  done
    1.16 +  by (auto simp add: Ex1_def Bex1_rel_def Bex_def Ball_def in_respects)
    1.17  
    1.18  lemma bex1_bexeq_reg_eqv:
    1.19    assumes a: "equivp R"