src/HOL/Divides.thy
changeset 53199 7a9fe70c8b0a
parent 53070 6a3410845bb2
child 53374 a14d2a854c02
     1.1 --- a/src/HOL/Divides.thy	Mon Aug 26 10:33:16 2013 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Aug 26 11:41:17 2013 +0200
     1.3 @@ -563,7 +563,6 @@
     1.4    qed
     1.5    moreover note assms w_exhaust
     1.6    ultimately have "w = 0" by auto
     1.7 -  find_theorems "_ + ?b < _ + ?b"
     1.8    with mod_w have mod: "a mod (2 * b) = a mod b" by simp
     1.9    have "2 * (a div (2 * b)) = a div b - w"
    1.10      by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)