--- a/src/HOL/Matrix_LP/Matrix.thy Fri Jul 29 08:22:59 2016 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy Fri Jul 29 20:34:07 2016 +0200
@@ -514,11 +514,12 @@
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 (cases "m = 0")
- apply (simp)
+ apply simp
apply (drule sube)
- apply (auto)
+ apply auto
apply (rule a)
- by (simp add: subc cong del: if_cong)
+ apply (simp add: subc cong del: if_weak_cong)
+ done
qed
then show ?thesis using assms by simp
qed