# HG changeset patch
# User wenzelm
# Date 1159382349 -7200
# Node ID 4ccef1ac4c9b08579c94095fe27dcb4af3726d38
# Parent  275f9bd2ead91c759158f93480b2ae21dfb63f60
removed redundant lemmas;

diff -r 275f9bd2ead9 -r 4ccef1ac4c9b src/HOL/Complex/ex/NSPrimes.thy
--- a/src/HOL/Complex/ex/NSPrimes.thy	Wed Sep 27 18:34:26 2006 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy	Wed Sep 27 20:39:09 2006 +0200
@@ -370,7 +370,7 @@
 apply (subgoal_tac "1 < N + 1")
 prefer 2 apply (blast intro: hypnat_add_one_gt_one)
 apply (drule hyperprime_factor_exists)
-apply (auto intro: STAR_mem)
+apply auto
 apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}")
 apply (force simp add: starprime_def, safe)
 apply (drule_tac x = x in bspec)