src/HOL/Matrix/Matrix.thy
changeset 28637 7aabaf1ba263
parent 28562 4e74209f113e
child 29667 53103fc8ffa3
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Oct 17 10:21:03 2008 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Oct 17 10:39:39 2008 +0200
     1.3 @@ -1293,7 +1293,7 @@
     1.4    le_matrix_def: "A \<le> B \<longleftrightarrow> (\<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i)"
     1.5  
     1.6  definition
     1.7 -  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
     1.8 +  less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A"
     1.9  
    1.10  instance ..
    1.11  
    1.12 @@ -1310,7 +1310,8 @@
    1.13  apply (rule ext)+
    1.14  apply (drule_tac x=xa in spec, drule_tac x=xa in spec)
    1.15  apply (drule_tac x=xb in spec, drule_tac x=xb in spec)
    1.16 -by simp
    1.17 +apply simp
    1.18 +done
    1.19  
    1.20  lemma le_apply_matrix:
    1.21    assumes