# HG changeset patch
# User obua
# Date 1113901171 -7200
# Node ID 38c8ea8521e776306011058ec7f9b0413051247d
# Parent  a167d50eadbb1c22e2c629fd8a191e83ac235a7a
Removed mult_commute axiom from comm_semiring axclass.

diff -r a167d50eadbb -r 38c8ea8521e7 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Tue Apr 19 00:14:27 2005 +0200
+++ b/src/HOL/Ring_and_Field.thy	Tue Apr 19 10:59:31 2005 +0200
@@ -31,7 +31,6 @@
 axclass semiring_0_cancel \<subseteq> semiring_0, cancel_ab_semigroup_add
 
 axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
-  mult_commute: "a * b = b * a"
   distrib: "(a + b) * c = a * c + b * c"
 
 instance comm_semiring \<subseteq> semiring