# HG changeset patch
# User chaieb
# Date 1093869809 -7200
# Node ID 66f0584aa7147f17b1c62f2741c5830c6b718615
# Parent  a1e84e86c583e98969dfe8209bfffa1841d283e6
commentar eliminated a line 156 - arith raised Match exception at m dvd 2

diff -r a1e84e86c583 -r 66f0584aa714 src/HOL/Complex/ex/NSPrimes.thy
--- 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]