--- a/src/HOL/Computational_Algebra/Field_as_Ring.thy Wed Oct 09 23:00:52 2019 +0200
+++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy Wed Oct 09 14:51:54 2019 +0000
@@ -35,7 +35,7 @@
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
@@ -66,7 +66,7 @@
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
@@ -97,7 +97,7 @@
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