src/HOL/Matrix/Matrix.thy
changeset 21312 1d39091a3208
parent 20633 e98f59806244
child 22422 ee19cdb07528
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Sat Nov 11 23:58:46 2006 +0100
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Sun Nov 12 19:22:10 2006 +0100
     1.3 @@ -20,10 +20,10 @@
     1.4    times_matrix_def: "A * B == mult_matrix (op *) (op +) A B"
     1.5  
     1.6  lemma is_meet_combine_matrix_meet: "is_meet (combine_matrix meet)"
     1.7 -  by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le meet_imp_le)
     1.8 +  by (simp_all add: is_meet_def le_matrix_def meet_left_le meet_right_le le_meetI)
     1.9  
    1.10  lemma is_join_combine_matrix_join: "is_join (combine_matrix join)"
    1.11 -  by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_imp_le)
    1.12 +  by (simp_all add: is_join_def le_matrix_def join_left_le join_right_le join_leI)
    1.13  
    1.14  instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    1.15  proof