Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/NumberTheory/Euler.thy
changeset 16733 236dfafbeb63
parent 16663 13e9c402308b
child 16974 0f8ebabf3163 
--- a/src/HOL/NumberTheory/Euler.thy	Thu Jul 07 12:36:56 2005 +0200
+++ b/src/HOL/NumberTheory/Euler.thy	Thu Jul 07 12:39:17 2005 +0200
@@ -175,7 +175,7 @@
 lemma SRStar_d22set_prop [rule_format]: "2 < p --> (SRStar p) = {1} \<union> 
     (d22set (p - 1))";
   apply (induct p rule: d22set.induct, auto)
-  apply (simp add: SRStar_def d22set.simps, arith)
+  apply (simp add: SRStar_def d22set.simps)
   apply (simp add: SRStar_def d22set.simps, clarify)
   apply (frule aux1)
   apply (frule aux2, auto)
isabelle