# HG changeset patch # User wenzelm # Date 1661979532 -7200 # Node ID 5f94db3a7e2507771e1594bb3e4a81362b3ba087 # Parent 105867f98630dc0da665741fcd5c95245a7049a6 eliminated tabs, assuming tab-width=4; diff -r 105867f98630 -r 5f94db3a7e25 src/HOL/Euclidean_Division.thy --- a/src/HOL/Euclidean_Division.thy Wed Aug 31 22:51:27 2022 +0200 +++ b/src/HOL/Euclidean_Division.thy Wed Aug 31 22:58:52 2022 +0200 @@ -2361,7 +2361,7 @@ by (auto simp add: t) ultimately show ?thesis by (simp add: divmod_def prod_eq_iff split_def Let_def - not_less mod_eq_0_iff_dvd Rings.mod_eq_0_iff_dvd False not_le *) + not_less mod_eq_0_iff_dvd Rings.mod_eq_0_iff_dvd False not_le *) (simp add: flip: of_nat_numeral of_nat_mult add.commute [of 1] of_nat_div of_nat_mod of_nat_Suc of_nat_diff) qed