src/HOL/ex/Dedekind_Real.thy
changeset 40822 98a5faa5aec0
parent 39910 10097e0a9dbd
child 41541 1fa4725c4656
     1.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Nov 30 15:58:21 2010 +0100
     1.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Nov 30 17:19:11 2010 +0100
     1.3 @@ -1288,7 +1288,7 @@
     1.4  proof -
     1.5    have "(\<lambda>z w. (\<lambda>(x,y). (\<lambda>(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)
     1.6          respects2 realrel"
     1.7 -    by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
     1.8 +    by (auto simp add: congruent2_def, blast intro: real_add_congruent2_lemma) 
     1.9    thus ?thesis
    1.10      by (simp add: real_add_def UN_UN_split_split_eq
    1.11                    UN_equiv_class2 [OF equiv_realrel equiv_realrel])
    1.12 @@ -1297,7 +1297,7 @@
    1.13  lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})"
    1.14  proof -
    1.15    have "(\<lambda>(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel"
    1.16 -    by (simp add: congruent_def add_commute) 
    1.17 +    by (auto simp add: congruent_def add_commute) 
    1.18    thus ?thesis
    1.19      by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel])
    1.20  qed