# HG changeset patch
# User haftmann
# Date 1174913581 -7200
# Node ID 21c221e1c8ebd6b2d3991fda1bf1ed1e6ef1a8fe
# Parent  2f4c974147462a25276cd0b6dbbccfdd5f46bde6
naming tuned

diff -r 2f4c97414746 -r 21c221e1c8eb src/HOL/Hyperreal/StarClasses.thy
--- a/src/HOL/Hyperreal/StarClasses.thy	Mon Mar 26 14:53:00 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Mon Mar 26 14:53:01 2007 +0200
@@ -401,7 +401,7 @@
 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_times_zero_less_eq_less.mult_strict_mono)
+by (intro_classes, transfer, rule ordered_comm_semiring_strict_class.plus_less_eq_less_zero_times.mult_strict_mono)
 
 instance star :: (pordered_ring) pordered_ring ..
 instance star :: (lordered_ring) lordered_ring ..