# HG changeset patch
# User obua
# Date 1084201841 -7200
# Node ID 021264410f8753e14e4ad05197c31df9146fcd66
# Parent  b77ce15b625abb7edc09096801514627845a39f5
preparation for integration with new Ring_and_Field.thy

diff -r b77ce15b625a -r 021264410f87 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Mon May 10 16:40:54 2004 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Mon May 10 17:10:41 2004 +0200
@@ -126,11 +126,6 @@
 instance g_almost_semiring < matrix_element
   by intro_classes simp
 
-instance semiring < g_semiring
-apply (intro_classes)
-apply (simp_all add: add_ac)
-by (simp_all add: mult_assoc left_distrib right_distrib)
-
 instance matrix :: (g_almost_semiring) g_almost_semiring
 apply (intro_classes)
 by (simp add: plus_matrix_def combine_matrix_def combine_infmatrix_def)
@@ -190,10 +185,6 @@
 
 axclass pordered_g_semiring < g_semiring, pordered_matrix_element
 
-instance almost_ordered_semiring < pordered_g_semiring
-apply (intro_classes)
-by (simp_all add: add_right_mono mult_right_mono mult_left_mono)
-
 instance matrix :: (pordered_g_semiring) pordered_g_semiring ..
 
 lemma nrows_mult: "nrows ((A::('a::matrix_element) matrix) * B) <= nrows A"
@@ -202,6 +193,7 @@
 lemma ncols_mult: "ncols ((A::('a::matrix_element) matrix) * B) <= ncols B"
 by (simp add: times_matrix_def mult_ncols)
 
+(*
 constdefs
   one_matrix :: "nat \<Rightarrow> ('a::semiring) matrix"
   "one_matrix n == Abs_matrix (% j i. if j = i & j < n then 1 else 0)"
@@ -253,5 +245,5 @@
 by (simp add: right_inverse_matrix_def)
 
 text {* to be continued \dots *}
-
+*)
 end