| changeset 15166 | 66f0584aa714 |
| parent 15149 | c5c4884634b7 |
| child 16663 | 13e9c402308b |
--- a/src/HOL/Complex/ex/NSPrimes.thy Mon Aug 30 14:40:18 2004 +0200 +++ b/src/HOL/Complex/ex/NSPrimes.thy Mon Aug 30 14:43:29 2004 +0200 @@ -153,7 +153,6 @@ apply (unfold prime_def, auto) apply (frule dvd_imp_le) apply (auto dest: dvd_0_left) -(*????arith raises exception Match!!??*) apply (case_tac m, simp, arith) done declare prime_two [simp]