# HG changeset patch
# User paulson
# Date 949660571 -3600
# Node ID 535d6253f930cc33bbb1421292968eb4ba1554c7
# Parent  61ec7bedc7175651f8dc659a3dabc2bb052e7b73
new theorem gcd_add_mult

diff -r 61ec7bedc717 -r 535d6253f930 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 **)