# HG changeset patch
# User paulson
# Date 1078911289 -3600
# Node ID d5c3d21df790fb61bb1a739ab059cdc62026ead5
# Parent  ba25d002a59c1e04828df23f15abcaae4cd631a9
strengthened the axclass claims

diff -r ba25d002a59c -r d5c3d21df790 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Mar 09 04:22:50 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Mar 10 10:34:49 2004 +0100
@@ -30,7 +30,7 @@
 lemmas plus_ac0 = plus_ac0.assoc plus_ac0.commute plus_ac0_left_commute
                   plus_ac0.zero plus_ac0_zero_right
 
-instance semiring < plus_ac0
+instance almost_semiring < plus_ac0
 proof qed (rule add_commute add_assoc almost_semiring.add_0)+
 
 axclass times_ac1 < times, one
@@ -59,7 +59,7 @@
   finally show ?thesis .
 qed
 
-instance semiring < times_ac1
+instance almost_semiring < times_ac1
   apply intro_classes
   apply (rule mult_commute)
   apply (rule mult_assoc, simp)