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.
removed redundant lemmas;
authorwenzelm
Wed, 27 Sep 2006 20:39:09 +0200
changeset 20733 4ccef1ac4c9b
parent 20732 275f9bd2ead9
child 20734 8aa9590bd452
removed redundant lemmas;
src/HOL/Complex/ex/NSPrimes.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle