src/HOL/Algebra/Divisibility.thy
changeset 68004 a8a20be7053a
parent 67443 3abf6a722518
child 68399 0b71d08528f0
     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Wed Apr 18 21:12:50 2018 +0100
     1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Thu Apr 19 14:49:08 2018 +0100
     1.3 @@ -2491,11 +2491,7 @@
     1.4    have "a' \<in> carrier G \<and> a' gcdof b c"
     1.5      apply (simp add: gcdof_greatestLower carr')
     1.6      apply (subst greatest_Lower_cong_l[of _ a])
     1.7 -        apply (simp add: a'a)
     1.8 -       apply (simp add: carr)
     1.9 -      apply (simp add: carr)
    1.10 -     apply (simp add: carr)
    1.11 -    apply (simp add: gcdof_greatestLower[symmetric] agcd carr)
    1.12 +        apply (simp_all add: a'a carr gcdof_greatestLower[symmetric] agcd)
    1.13      done
    1.14    then show ?thesis ..
    1.15  qed