# HG changeset patch
# User wenzelm
# Date 1377510077 -7200
# Node ID 7a9fe70c8b0a28a4e9fc06d6608d50e4a76ffab1
# Parent  06b096cf89ca6acc36a109e5694497d3f2069aa8
removed junk;

diff -r 06b096cf89ca -r 7a9fe70c8b0a src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Aug 26 10:33:16 2013 +0200
+++ b/src/HOL/Divides.thy	Mon Aug 26 11:41:17 2013 +0200
@@ -563,7 +563,6 @@
   qed
   moreover note assms w_exhaust
   ultimately have "w = 0" by auto
-  find_theorems "_ + ?b < _ + ?b"
   with mod_w have mod: "a mod (2 * b) = a mod b" by simp
   have "2 * (a div (2 * b)) = a div b - w"
     by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)