--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Nov 09 13:49:56 2015 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Mon Nov 09 15:48:17 2015 +0100
@@ -238,7 +238,7 @@
shows "c = gcd a b"
by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
-sublocale gcd!: abel_semigroup gcd
+sublocale gcd: abel_semigroup gcd
proof
fix a b c
show "gcd (gcd a b) c = gcd a (gcd b c)"
@@ -790,7 +790,7 @@
shows "c = lcm a b"
by (rule associated_eqI) (auto simp: assms intro: lcm_least)
-sublocale lcm!: abel_semigroup lcm ..
+sublocale lcm: abel_semigroup lcm ..
lemma dvd_lcm_D1:
"lcm m n dvd k \<Longrightarrow> m dvd k"