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/Big_Operators.thy
changeset 49962 a8cc904a6820
parent 49715 16d8c6d288bc
child 51112 da97167e03f7 
--- a/src/HOL/Big_Operators.thy	Fri Oct 19 10:46:42 2012 +0200
+++ b/src/HOL/Big_Operators.thy	Fri Oct 19 15:12:52 2012 +0200
@@ -699,7 +699,7 @@
   proof induct
     case empty thus ?case by simp
   next
-    case (insert x A) thus ?case by (simp add: right_distrib)
+    case (insert x A) thus ?case by (simp add: distrib_left)
   qed
 next
   case False thus ?thesis by (simp add: setsum_def)
@@ -713,7 +713,7 @@
   proof induct
     case empty thus ?case by simp
   next
-    case (insert x A) thus ?case by (simp add: left_distrib)
+    case (insert x A) thus ?case by (simp add: distrib_right)
   qed
 next
   case False thus ?thesis by (simp add: setsum_def)
isabelle