--- a/src/HOL/Library/Code_Binary_Nat.thy Sun Aug 21 06:18:23 2022 +0000
+++ b/src/HOL/Library/Code_Binary_Nat.thy Sun Aug 21 06:18:23 2022 +0000
@@ -127,13 +127,13 @@
"nat_of_num k < nat_of_num l \<longleftrightarrow> k < l"
by (simp_all add: nat_of_num_numeral)
-declare [[code drop: Divides.divmod_nat]]
+declare [[code drop: Euclidean_Division.divmod_nat]]
lemma divmod_nat_code [code]:
- "Divides.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
- "Divides.divmod_nat m 0 = (0, m)"
- "Divides.divmod_nat 0 n = (0, 0)"
- by (simp_all add: prod_eq_iff nat_of_num_numeral)
+ "Euclidean_Division.divmod_nat (nat_of_num k) (nat_of_num l) = divmod k l"
+ "Euclidean_Division.divmod_nat m 0 = (0, m)"
+ "Euclidean_Division.divmod_nat 0 n = (0, 0)"
+ by (simp_all add: Euclidean_Division.divmod_nat_def nat_of_num_numeral)
end