# HG changeset patch
# User haftmann
# Date 1282136110 -7200
# Node ID a9ce311eb6b98f03259a9246ecf7c4fc493fb4be
# Parent  324219de6ee3b7c8213183ef6ea2b4547989303b
tuned proof

diff -r 324219de6ee3 -r a9ce311eb6b9 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Wed Aug 18 14:55:09 2010 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Wed Aug 18 14:55:10 2010 +0200
@@ -528,12 +528,12 @@
       show "f (s 0) (foldseq f (\<lambda>k. if k < m then s (Suc k) else foldseq f (\<lambda>k. s (Suc (k + m))) (na - m)) m) =
         foldseq f (\<lambda>k. if k < m then s k else foldseq f (\<lambda>k. s (k + m)) (Suc na - m)) m"
         apply (simp add: subd)
-        apply (case_tac "m=0")
+        apply (cases "m = 0")
         apply (simp)
         apply (drule sube)
         apply (auto)
         apply (rule a)
-        by (simp add: subc if_def)
+        by (simp add: subc cong del: if_cong)
     qed
   then show ?thesis using assms by simp
 qed