src/HOL/GCD.thy
changeset 61605 1bf7b186542e
parent 61566 c3d6e570ccef
child 61649 268d88ec9087
     1.1 --- a/src/HOL/GCD.thy	Mon Nov 09 13:49:56 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Mon Nov 09 15:48:17 2015 +0100
     1.3 @@ -104,7 +104,7 @@
     1.4    "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
     1.5    by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
     1.6  
     1.7 -sublocale gcd!: abel_semigroup gcd
     1.8 +sublocale gcd: abel_semigroup gcd
     1.9  proof
    1.10    fix a b c
    1.11    show "gcd a b = gcd b a"
    1.12 @@ -256,7 +256,7 @@
    1.13    "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
    1.14    by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
    1.15  
    1.16 -sublocale lcm!: abel_semigroup lcm
    1.17 +sublocale lcm: abel_semigroup lcm
    1.18  proof
    1.19    fix a b c
    1.20    show "lcm a b = lcm b a"