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/WilsonRuss.thy
changeset 15236 f289e8ba2bb3
parent 15197 19e735596e51
child 15392 290bc97038c7 
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -136,7 +136,7 @@
     "[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
   apply (induct z)
    apply (auto simp add: zpower_zadd_distrib)
-  apply (subgoal_tac "zcong (x^y * x^(y * n)) (1 * 1) p")
+  apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p")
    apply (rule_tac [2] zcong_zmult, simp_all)
   done
isabelle