--- a/src/HOL/Matrix/MatrixGeneral.thy Wed Feb 02 18:06:00 2005 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy Wed Feb 02 18:06:25 2005 +0100
@@ -698,11 +698,11 @@
let ?mx = "max (ncols a) (max (nrows u) (nrows v))"
from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
combine_matrix fadd (mult_matrix_n (max (ncols a) (nrows u)) fmul fadd a u) (mult_matrix_n (max (ncols a) (nrows v)) fmul fadd a v)"
- apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+ apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
apply (simp add: max1 max2 combine_nrows combine_ncols)+
- apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+ apply (subst mult_matrix_nm[of _ _ v ?mx fadd fmul])
apply (simp add: max1 max2 combine_nrows combine_ncols)+
- apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+ apply (subst mult_matrix_nm[of _ _ u ?mx fadd fmul])
apply (simp add: max1 max2 combine_nrows combine_ncols)+
apply (simp add: mult_matrix_n_def r_distributive_def foldseq_distr[of fadd])
apply (simp add: combine_matrix_def combine_infmatrix_def)
@@ -738,9 +738,9 @@
let ?mx = "max (nrows a) (max (ncols u) (ncols v))"
from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
combine_matrix fadd (mult_matrix_n (max (ncols u) (nrows a)) fmul fadd u a) (mult_matrix_n (max (ncols v) (nrows a)) fmul fadd v a)"
- apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+ apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul])
apply (simp add: max1 max2 combine_nrows combine_ncols)+
- apply (simplesubst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
+ apply (subst mult_matrix_nm[of u _ _ ?mx fadd fmul])
apply (simp add: max1 max2 combine_nrows combine_ncols)+
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
apply (simp add: max1 max2 combine_nrows combine_ncols)+
@@ -1227,7 +1227,7 @@
have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
by (simp! add: associative_def commutative_def)
then show ?concl
- apply (simplesubst mult_matrix_assoc)
+ apply (subst mult_matrix_assoc)
apply (simp_all!)
by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+
qed