src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 62348 9a5f43dac883
parent 61605 1bf7b186542e
child 62353 7f927120b5a2
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -1200,7 +1200,7 @@
     1.4  qed
     1.5  
     1.6  subclass semiring_Gcd
     1.7 -  by standard (simp_all add: Gcd_greatest)
     1.8 +  by standard (auto intro: Gcd_greatest Lcm_least)
     1.9  
    1.10  lemma GcdI:
    1.11    assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
    1.12 @@ -1212,9 +1212,6 @@
    1.13    "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
    1.14    by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest)
    1.15  
    1.16 -subclass semiring_Lcm
    1.17 -  by standard (simp add: Lcm_Gcd)
    1.18 -
    1.19  lemma Gcd_1:
    1.20    "1 \<in> A \<Longrightarrow> Gcd A = 1"
    1.21    by (auto intro!: Gcd_eq_1_I)