src/HOL/ex/Primes.ML

--- a/src/HOL/ex/Primes.ML	Wed Feb 02 20:19:25 2000 +0100
+++ b/src/HOL/ex/Primes.ML	Fri Feb 04 11:36:11 2000 +0100
@@ -181,6 +181,12 @@
 by (asm_simp_tac (simpset() addsimps [add_commute, gcd_add]) 1);
 qed "gcd_add2";
 
+Goal "gcd(m, k*m+n) = gcd(m,n)";
+by (induct_tac "k" 1);
+by (asm_simp_tac (simpset() addsimps [gcd_add, add_assoc]) 2); 
+by (Simp_tac 1);
+qed "gcd_add_mult";
+
 
 (** More multiplication laws **)