diff -r 7187373c6cb1 -r 53103fc8ffa3 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/Library/Float.thy	Wed Jan 28 16:29:16 2009 +0100
@@ -38,7 +38,7 @@
   show ?thesis
   proof (induct a)
     case (1 n)
-    from pos show ?case by (simp add: ring_simps)
+    from pos show ?case by (simp add: algebra_simps)
   next
     case (2 n)
     show ?case
@@ -59,7 +59,7 @@
     show ?case by simp
   next
     case (Suc m)
-    show ?case by (auto simp add: ring_simps pow2_add1 prems)
+    show ?case by (auto simp add: algebra_simps pow2_add1 prems)
   qed
 next
   case (2 n)
@@ -72,7 +72,7 @@
       apply (subst pow2_neg[of "-1"])
       apply (simp)
       apply (insert pow2_add1[of "-a"])
-      apply (simp add: ring_simps)
+      apply (simp add: algebra_simps)
       apply (subst pow2_neg[of "-a"])
       apply (simp)
       done
@@ -83,7 +83,7 @@
       apply (auto)
       apply (subst pow2_neg[of "a + (-2 - int m)"])
       apply (subst pow2_neg[of "-2 - int m"])
-      apply (auto simp add: ring_simps)
+      apply (auto simp add: algebra_simps)
       apply (subst a)
       apply (subst b)
       apply (simp only: pow2_add1)
@@ -91,13 +91,13 @@
       apply (subst pow2_neg[of "int m + 1"])
       apply auto
       apply (insert prems)
-      apply (auto simp add: ring_simps)
+      apply (auto simp add: algebra_simps)
       done
   qed
 qed
 
 lemma "float (a, e) + float (b, e) = float (a + b, e)"
-by (simp add: float_def ring_simps)
+by (simp add: float_def algebra_simps)
 
 definition
   int_of_real :: "real \<Rightarrow> int" where
@@ -254,7 +254,7 @@
 
 lemma float_transfer_even: "even a \<Longrightarrow> float (a, b) = float (a div 2, b+1)"
   apply (subst float_transfer[where a="a" and b="b" and c="-1", simplified])
-  apply (simp_all add: pow2_def even_def real_is_int_def ring_simps)
+  apply (simp_all add: pow2_def even_def real_is_int_def algebra_simps)
   apply (auto)
 proof -
   fix q::int
@@ -319,7 +319,7 @@
   "float (a1, e1) + float (a2, e2) =
   (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
   else float (a1*2^(nat (e1-e2))+a2, e2))"
-  apply (simp add: float_def ring_simps)
+  apply (simp add: float_def algebra_simps)
   apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
   done