--- a/src/HOL/GCD.thy Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/GCD.thy Tue Feb 24 11:12:58 2009 -0800
@@ -60,9 +60,12 @@
lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
by simp
-lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1"
+lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
by simp
+lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
+ unfolding One_nat_def by (rule gcd_1)
+
declare gcd.simps [simp del]
text {*
@@ -116,9 +119,12 @@
apply (blast intro: dvd_trans)
done
-lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1"
+lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
by (simp add: gcd_commute)
+lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
+ unfolding One_nat_def by (rule gcd_1_left)
+
text {*
\medskip Multiplication laws
*}