--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Feb 17 21:51:57 2016 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Feb 17 21:51:57 2016 +0100
@@ -1200,7 +1200,7 @@
qed
subclass semiring_Gcd
- by standard (simp_all add: Gcd_greatest)
+ by standard (auto intro: Gcd_greatest Lcm_least)
lemma GcdI:
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"
@@ -1212,9 +1212,6 @@
"Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest)
-subclass semiring_Lcm
- by standard (simp add: Lcm_Gcd)
-
lemma Gcd_1:
"1 \<in> A \<Longrightarrow> Gcd A = 1"
by (auto intro!: Gcd_eq_1_I)