diff -r 2c76042c3b06 -r 9fbce4042034 src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Mon Nov 26 18:34:17 2001 +0100
+++ b/src/HOL/Library/Primes.thy	Mon Nov 26 23:23:33 2001 +0100
@@ -63,16 +63,13 @@
   conjunctions don't seem provable separately.
 *}
 
-lemma gcd_dvd_both: "gcd (m, n) dvd m \<and> gcd (m, n) dvd n"
+lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
+  and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
   apply (induct m n rule: gcd_induct)
    apply (simp_all add: gcd_non_0)
   apply (blast dest: dvd_mod_imp_dvd)
   done
 
-lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
-lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
-
-
 text {*
   \medskip Maximality: for all @{term m}, @{term n}, @{term k}
   naturals, if @{term k} divides @{term m} and @{term k} divides