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)"
```