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/Binomial_Plus.thy
changeset 80276 360e6217cda6
parent 80177 1478555580af 
--- a/src/HOL/Binomial_Plus.thy	Thu Jun 06 23:12:04 2024 +0200
+++ b/src/HOL/Binomial_Plus.thy	Thu Jun 06 23:19:59 2024 +0200
@@ -223,7 +223,7 @@
 proof -
   have dvd: "y \<noteq> 0 \<Longrightarrow> ((of_int (x div y))::'a::field_char_0) = of_int x / of_int y \<Longrightarrow> y dvd x"
     for x y :: int
-    by (smt dvd_triv_left mult.commute nonzero_eq_divide_eq of_int_eq_0_iff of_int_eq_iff of_int_mult)
+    by (metis dvd_triv_right nonzero_eq_divide_eq of_int_0_eq_iff of_int_eq_iff of_int_mult)
   show ?thesis
   proof (cases "0 < a")
     case True
isabelle