src/HOL/Matrix/Matrix.thy
changeset 14691 e1eedc8cad37
parent 14662 d2c6a0f030ab
child 14724 021264410f87
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Sat May 01 21:59:12 2004 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Sat May 01 22:01:57 2004 +0200
     1.3 @@ -20,11 +20,8 @@
     1.4  axclass matrix_element < almost_matrix_element
     1.5  matrix_add_0[simp]: "0+0 = 0"
     1.6  
     1.7 -instance matrix :: (plus) plus
     1.8 -by (intro_classes)
     1.9 -
    1.10 -instance matrix :: (times) times
    1.11 -by (intro_classes)
    1.12 +instance matrix :: (plus) plus ..
    1.13 +instance matrix :: (times) times ..
    1.14  
    1.15  defs (overloaded)
    1.16  plus_matrix_def: "A + B == combine_matrix (op +) A B"
    1.17 @@ -127,7 +124,7 @@
    1.18  g_add_leftimp_eq: "a+b = a+c \<Longrightarrow> b = c"
    1.19  
    1.20  instance g_almost_semiring < matrix_element
    1.21 -by (intro_classes, simp)
    1.22 +  by intro_classes simp
    1.23  
    1.24  instance semiring < g_semiring
    1.25  apply (intro_classes)
    1.26 @@ -197,8 +194,7 @@
    1.27  apply (intro_classes)
    1.28  by (simp_all add: add_right_mono mult_right_mono mult_left_mono)
    1.29  
    1.30 -instance matrix :: (pordered_g_semiring) pordered_g_semiring
    1.31 -by (intro_classes)
    1.32 +instance matrix :: (pordered_g_semiring) pordered_g_semiring ..
    1.33  
    1.34  lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
    1.35  by (simp add: times_matrix_def mult_nrows)