Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Divides.thy
changeset 80452 0303b3a0edde
parent 78937 5e6b195eee83 
--- 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
isabelle