changeset 5148 | 74919e8f221c |
parent 5143 | b94cd208f073 |
child 5227 | e5a6ace920a0 |
--- a/src/HOL/ex/Primes.ML Wed Jul 15 14:13:18 1998 +0200 +++ b/src/HOL/ex/Primes.ML Wed Jul 15 14:19:02 1998 +0200 @@ -90,7 +90,7 @@ (*USED??*) Goalw [is_gcd_def] - "!!m n. [| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"; + "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"; by (Blast_tac 1); qed "is_gcd_dvd";