src/HOL/Matrix/Matrix.thy

 lemma nrows_singleton[simp]: "nrows(singleton_matrix j i e) = (if e = 0 then 0 else Suc j)"
 proof-
 have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
 from th show ?thesis 
 apply (auto)
-apply (rule le_anti_sym)
+apply (rule le_antisym)
 apply (subst nrows_le)
 apply (simp add: singleton_matrix_def, auto)
 apply (subst RepAbs_matrix)
 apply auto
 apply (simp add: Suc_le_eq)

 lemma ncols_singleton[simp]: "ncols(singleton_matrix j i e) = (if e = 0 then 0 else Suc i)"
 proof-
 have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
 from th show ?thesis 
 apply (auto)
-apply (rule le_anti_sym)
+apply (rule le_antisym)
 apply (subst ncols_le)
 apply (simp add: singleton_matrix_def, auto)
 apply (subst RepAbs_matrix)
 apply auto
 apply (simp add: Suc_le_eq)

   apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)
   apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+)
   apply (subst foldseq_almostzero[of _ j])
   apply (simp add: prems)+
   apply (auto)
-  apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
+  apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
   done
 
 lemma mult_matrix_ext:
   assumes
   eprem: