removed junk;
authorwenzelm
Mon Aug 26 11:41:17 2013 +0200 (2013-08-26)
changeset 531997a9fe70c8b0a
parent 53198 06b096cf89ca
child 53200 09e8c42dbb06
removed junk;
src/HOL/Divides.thy
     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)