src/HOL/GCD.thy
changeset 37770 cddb3106adb8
parent 36350 bc7982c54e37
child 41550 efa734d9b221
     1.1 --- a/src/HOL/GCD.thy	Mon Jul 12 11:21:56 2010 +0200
     1.2 +++ b/src/HOL/GCD.thy	Mon Jul 12 11:39:27 2010 +0200
     1.3 @@ -302,11 +302,11 @@
     1.4  lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
     1.5    by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
     1.6  
     1.7 -interpretation gcd_nat!: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
     1.8 +interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
     1.9  proof
    1.10  qed (auto intro: dvd_antisym dvd_trans)
    1.11  
    1.12 -interpretation gcd_int!: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    1.13 +interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
    1.14  proof
    1.15  qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
    1.16  
    1.17 @@ -1383,7 +1383,7 @@
    1.18      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    1.19    by (auto intro: dvd_antisym [transferred] lcm_least_int)
    1.20  
    1.21 -interpretation lcm_nat!: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.22 +interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.23  proof
    1.24    fix n m p :: nat
    1.25    show "lcm (lcm n m) p = lcm n (lcm m p)"
    1.26 @@ -1392,7 +1392,7 @@
    1.27      by (simp add: lcm_nat_def gcd_commute_nat field_simps)
    1.28  qed
    1.29  
    1.30 -interpretation lcm_int!: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
    1.31 +interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
    1.32  proof
    1.33    fix n m p :: int
    1.34    show "lcm (lcm n m) p = lcm n (lcm m p)"