src/HOL/Multivariate_Analysis/Determinants.thy
changeset 47108 2a1953f0d20d
parent 44457 d366fa5551ef
child 50526 899c9c4e4a4c
     1.1 --- a/src/HOL/Multivariate_Analysis/Determinants.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -286,7 +286,7 @@
     1.4  proof-
     1.5    have tha: "\<And>(a::'a) b. a = b ==> b = - a ==> a = 0"
     1.6      by simp
     1.7 -  have th1: "of_int (-1) = - 1" by (metis of_int_1 of_int_minus number_of_Min)
     1.8 +  have th1: "of_int (-1) = - 1" by simp
     1.9    let ?p = "Fun.swap i j id"
    1.10    let ?A = "\<chi> i. A $ ?p i"
    1.11    from r have "A = ?A" by (simp add: vec_eq_iff row_def swap_def)
    1.12 @@ -1058,8 +1058,7 @@
    1.13    unfolding det_def UNIV_2
    1.14    unfolding setsum_over_permutations_insert[OF f12]
    1.15    unfolding permutes_sing
    1.16 -  apply (simp add: sign_swap_id sign_id swap_id_eq)
    1.17 -  by (simp add: arith_simps(31)[symmetric] del: arith_simps(31))
    1.18 +  by (simp add: sign_swap_id sign_id swap_id_eq)
    1.19  qed
    1.20  
    1.21  lemma det_3: "det (A::'a::comm_ring_1^3^3) =
    1.22 @@ -1079,9 +1078,7 @@
    1.23    unfolding setsum_over_permutations_insert[OF f23]
    1.24  
    1.25    unfolding permutes_sing
    1.26 -  apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
    1.27 -  apply (simp add: arith_simps(31)[symmetric] del: arith_simps(31))
    1.28 -  by (simp add: field_simps)
    1.29 +  by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
    1.30  qed
    1.31  
    1.32  end