Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
commentar eliminated a line 156 - arith raised Match exception at m dvd 2
authorchaieb
Mon, 30 Aug 2004 14:43:29 +0200
changeset 15166 66f0584aa714
parent 15165 a1e84e86c583
child 15167 67f9c3855715
commentar eliminated a line 156 - arith raised Match exception at m dvd 2
src/HOL/Complex/ex/NSPrimes.thy file | annotate | diff | comparison | revisions 
--- 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]
isabelle