# HG changeset patch
# User haftmann
# Date 1219990498 -7200
# Node ID 295a8fc9268436bf4383a1b239f1c6573bc84465
# Parent  309c0a92e0da635bef95b8eb5862364afa0ea5ab
fixed names of class assumptions

diff -r 309c0a92e0da -r 295a8fc92684 src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Fri Aug 29 07:43:25 2008 +0200
+++ b/src/HOL/NSA/StarDef.thy	Fri Aug 29 08:14:58 2008 +0200
@@ -824,7 +824,7 @@
 by (intro_classes, transfer, rule mult_commute)
 
 instance star :: (comm_monoid_add) comm_monoid_add
-by (intro_classes, transfer, rule comm_monoid_add_class.zero_plus.add_0)
+by (intro_classes, transfer, rule comm_monoid_add_class.add_0)
 
 instance star :: (monoid_mult) monoid_mult
 apply (intro_classes)
@@ -941,12 +941,12 @@
 done
 
 instance star :: (pordered_comm_semiring) pordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.less_eq_less_times_zero.mult_mono1)
+by (intro_classes, transfer, rule mult_mono1_class.mult_mono1)
 
 instance star :: (pordered_cancel_comm_semiring) pordered_cancel_comm_semiring ..
 
 instance star :: (ordered_comm_semiring_strict) ordered_comm_semiring_strict
-by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_less_eq_less_zero_times.mult_strict_left_mono_comm)
+by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.mult_strict_left_mono_comm)
 
 instance star :: (pordered_ring) pordered_ring ..
 instance star :: (pordered_ring_abs) pordered_ring_abs
diff -r 309c0a92e0da -r 295a8fc92684 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Fri Aug 29 07:43:25 2008 +0200
+++ b/src/HOL/Word/BinBoolList.thy	Fri Aug 29 08:14:58 2008 +0200
@@ -298,7 +298,7 @@
    apply clarsimp
   apply clarsimp
   apply safe
-   apply (erule allE, erule less_eq_less.order_trans [rotated],
+   apply (erule allE, erule preorder_class.order_trans [rotated],
           simp add: numeral_simps ring_simps cong add : number_of_False_cong)+
   done
 
diff -r 309c0a92e0da -r 295a8fc92684 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Fri Aug 29 07:43:25 2008 +0200
+++ b/src/HOL/Word/WordArith.thy	Fri Aug 29 08:14:58 2008 +0200
@@ -301,7 +301,7 @@
   by (auto simp: word_of_int_hom_syms [symmetric]
                  zadd_0_right add_commute add_assoc add_left_commute
                  mult_commute mult_assoc mult_left_commute
-                 plus_times.left_distrib plus_times.right_distrib)
+                 left_distrib right_distrib)
   
 lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute
 lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute