changeset 12300 9fbce4042034
parent 11701 3d51fbf81c17
child 12739 1fce8f51034d
--- 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)
-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