src/HOL/Matrix/Matrix.thy
changeset 33657 a4179bf442d1
parent 32960 69916a850301
child 34872 6ca970cfa873
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Thu Nov 12 14:32:21 2009 -0800
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Nov 13 14:14:04 2009 +0100
     1.3 @@ -873,7 +873,7 @@
     1.4  have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
     1.5  from th show ?thesis 
     1.6  apply (auto)
     1.7 -apply (rule le_anti_sym)
     1.8 +apply (rule le_antisym)
     1.9  apply (subst nrows_le)
    1.10  apply (simp add: singleton_matrix_def, auto)
    1.11  apply (subst RepAbs_matrix)
    1.12 @@ -889,7 +889,7 @@
    1.13  have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
    1.14  from th show ?thesis 
    1.15  apply (auto)
    1.16 -apply (rule le_anti_sym)
    1.17 +apply (rule le_antisym)
    1.18  apply (subst ncols_le)
    1.19  apply (simp add: singleton_matrix_def, auto)
    1.20  apply (subst RepAbs_matrix)
    1.21 @@ -1004,7 +1004,7 @@
    1.22    apply (subst foldseq_almostzero[of _ j])
    1.23    apply (simp add: prems)+
    1.24    apply (auto)
    1.25 -  apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
    1.26 +  apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
    1.27    done
    1.28  
    1.29  lemma mult_matrix_ext: