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/Decision_Procs/Commutative_Ring.thy
changeset 58834 773b378d9313
parent 58770 ae5e9b4f8daf
child 58889 5b7a9633cfa8 
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 30 16:36:44 2014 +0000
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Oct 30 21:02:01 2014 +0100
@@ -269,7 +269,7 @@
         by (simp add: even_pow sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] even_two_times_div_two)
     next
       case False with * show ?thesis
-        by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric] odd_two_times_div_two_Suc)
+        by (simp add: odd_pow mul_ci sqr_ci power_mult_distrib power_add [symmetric] mult_2 [symmetric] power_Suc [symmetric])
     qed
   qed
 qed
isabelle