--- a/src/HOL/GCD.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/GCD.thy Tue Nov 19 10:05:53 2013 +0100
@@ -134,6 +134,14 @@
lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
by (simp add: gcd_int_def)
+lemma gcd_neg_numeral_1_int [simp]:
+ "gcd (- numeral n :: int) x = gcd (numeral n) x"
+ by (fact gcd_neg1_int)
+
+lemma gcd_neg_numeral_2_int [simp]:
+ "gcd x (- numeral n :: int) = gcd x (numeral n)"
+ by (fact gcd_neg2_int)
+
lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
by(simp add: gcd_int_def)