# 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