src/HOL/Computational_Algebra/Field_as_Ring.thy

 definition [simp]: "euclidean_size_real = (euclidean_size_field :: real \<Rightarrow> _)"
 definition [simp]: "division_segment (x :: real) = 1"
 
 instance
   by standard
-    (simp_all add: dvd_field_iff divide_simps split: if_splits)
+    (simp_all add: dvd_field_iff field_split_simps split: if_splits)
 
 end
 
 instantiation real :: euclidean_ring_gcd
 begin

 definition [simp]: "euclidean_size_rat = (euclidean_size_field :: rat \<Rightarrow> _)"
 definition [simp]: "division_segment (x :: rat) = 1"
 
 instance
   by standard
-    (simp_all add: dvd_field_iff divide_simps split: if_splits)
+    (simp_all add: dvd_field_iff field_split_simps split: if_splits)
 
 end
 
 instantiation rat :: euclidean_ring_gcd
 begin

 definition [simp]: "euclidean_size_complex = (euclidean_size_field :: complex \<Rightarrow> _)"
 definition [simp]: "division_segment (x :: complex) = 1"
 
 instance
   by standard
-    (simp_all add: dvd_field_iff divide_simps split: if_splits)
+    (simp_all add: dvd_field_iff field_split_simps split: if_splits)
 
 end
 
 instantiation complex :: euclidean_ring_gcd
 begin