--- a/src/HOL/Divides.thy Fri Jun 28 23:53:48 2024 +0200
+++ b/src/HOL/Divides.thy Thu Jun 27 16:52:17 2024 +0000
@@ -108,8 +108,7 @@
context
begin
-(* REVISIT: should this be generalized to all semiring_div types? *)
-qualified lemma zmod_eq_0D [dest!]: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
+qualified lemma zmod_eq_0D: "\<exists>q. m = d * q" if "m mod d = 0" for m d :: int
using that by auto
qualified lemma div_geq [no_atp]: "m div n = Suc ((m - n) div n)" if "0 < n" and " \<not> m < n" for m n :: nat
--- a/src/HOL/Library/Float.thy Fri Jun 28 23:53:48 2024 +0200
+++ b/src/HOL/Library/Float.thy Thu Jun 27 16:52:17 2024 +0000
@@ -1348,7 +1348,6 @@
l_def[symmetric, THEN meta_eq_to_obj_eq]
apply transfer
apply (auto simp add: round_up_def truncate_up_rat_precision)
- apply (metis dvd_triv_left of_nat_dvd_iff)
apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
done
next
@@ -1364,7 +1363,6 @@
l_def[symmetric, THEN meta_eq_to_obj_eq]
apply transfer
apply (auto simp add: round_up_def ceil_divide_floor_conv truncate_up_rat_precision)
- apply (metis dvd_triv_left of_nat_dvd_iff)
apply (metis floor_divide_of_int_eq of_int_of_nat_eq)
done
qed