# HG changeset patch
# User haftmann
# Date 1719507137 0
# Node ID 0303b3a0eddef98ac573f1f26ed0f8ef96310fa7
# Parent  e0bd9e4811ad0c88edcf0fffdf6a5b179d21fc6a
dropped dubious dest rule which always unfolds a definition in the assumptions

diff -r e0bd9e4811ad -r 0303b3a0edde src/HOL/Divides.thy
--- 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
diff -r e0bd9e4811ad -r 0303b3a0edde src/HOL/Library/Float.thy
--- 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