src/HOL/Real.thy

   unfolding cr_real_eq rel_fun_def by (simp split: split_if_asm, metis)
 
 instance proof
   fix a b c :: real
   show "a + b = b + a"
-    by transfer (simp add: add_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "(a + b) + c = a + (b + c)"
-    by transfer (simp add: add_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "0 + a = a"
     by transfer (simp add: realrel_def)
   show "- a + a = 0"
     by transfer (simp add: realrel_def)
   show "a - b = a + - b"
     by (rule minus_real_def)
   show "(a * b) * c = a * (b * c)"
-    by transfer (simp add: mult_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "a * b = b * a"
-    by transfer (simp add: mult_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "1 * a = a"
-    by transfer (simp add: mult_ac realrel_def)
+    by transfer (simp add: ac_simps realrel_def)
   show "(a + b) * c = a * c + b * c"
     by transfer (simp add: distrib_right realrel_def)
   show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
     by transfer (simp add: realrel_def)
   show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"

 lemma le_Real:
   assumes X: "cauchy X" and Y: "cauchy Y"
   shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
 unfolding not_less [symmetric, where 'a=real] less_real_def
 apply (simp add: diff_Real not_positive_Real X Y)
-apply (simp add: diff_le_eq add_ac)
+apply (simp add: diff_le_eq ac_simps)
 done
 
 lemma le_RealI:
   assumes Y: "cauchy Y"
   shows "\<forall>n. x \<le> of_rat (Y n) \<Longrightarrow> x \<le> Real Y"