1.1 --- a/src/HOL/Matrix/Matrix.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4  
     1.5  (*
     1.6  constdefs
     1.7 -  one_matrix :: "nat \<Rightarrow> ('a::semiring) matrix"
     1.8 +  one_matrix :: "nat \<Rightarrow> ('a::comm_semiring_1_cancel) matrix"
     1.9    "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
    1.10  
    1.11  lemma Rep_one_matrix[simp]: "Rep_matrix (one_matrix n) j i = (if (j = i & j < n) then 1 else 0)"
    1.12 @@ -235,9 +235,9 @@
    1.13  by (simp add: max_def nrows)
    1.14  
    1.15  constdefs
    1.16 -  right_inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
    1.17 +  right_inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
    1.18    "right_inverse_matrix A X == (A * X = one_matrix (max (nrows A) (ncols X)))"
    1.19 -  inverse_matrix :: "('a::semiring) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
    1.20 +  inverse_matrix :: "('a::comm_semiring_1_cancel) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
    1.21    "inverse_matrix A X == (right_inverse_matrix A X) \<and> (right_inverse_matrix X A)"
    1.22  
    1.23  lemma right_inverse_matrix_dim: "right_inverse_matrix A X \<Longrightarrow> nrows A = ncols X"