# HG changeset patch
# User haftmann
# Date 1241762411 -7200
# Node ID d87465cbfc9e0ad6a78c9e23f889c97043f817fc
# Parent  ce37d8f48a9f1a13bff1396c90e1477730ca9000
moved int_factor_simprocs.ML to theory Int

diff -r ce37d8f48a9f -r d87465cbfc9e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu May 07 16:22:35 2009 +0200
+++ b/src/HOL/Int.thy	Fri May 08 08:00:11 2009 +0200
@@ -15,6 +15,9 @@
   "~~/src/Provers/Arith/assoc_fold.ML"
   "~~/src/Provers/Arith/cancel_numerals.ML"
   "~~/src/Provers/Arith/combine_numerals.ML"
+  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+  "~~/src/Provers/Arith/extract_common_term.ML"
+  ("Tools/int_factor_simprocs.ML")
   ("Tools/int_arith.ML")
 begin
 
@@ -1517,10 +1520,11 @@
 
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
+use "Tools/int_factor_simprocs.ML"
 
 setup {*
   ReorientProc.add
-    (fn Const(@{const_name number_of}, _) $ _ => true | _ => false)
+    (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
 *}
 
 simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
diff -r ce37d8f48a9f -r d87465cbfc9e src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Thu May 07 16:22:35 2009 +0200
+++ b/src/HOL/IntDiv.thy	Fri May 08 08:00:11 2009 +0200
@@ -8,10 +8,6 @@
 
 theory IntDiv
 imports Int Divides FunDef
-uses
-  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
-  "~~/src/Provers/Arith/extract_common_term.ML"
-  ("Tools/int_factor_simprocs.ML")
 begin
 
 definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
@@ -724,7 +720,6 @@
       apply (auto simp add: divmod_rel_def) 
       apply (auto simp add: algebra_simps)
       apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
-      apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
       done
     moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
     ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
@@ -1078,8 +1073,6 @@
    prefer 2
    apply (blast intro: order_less_trans)
   apply (simp add: zero_less_mult_iff)
-  apply (subgoal_tac "n * k < n * 1")
-   apply (drule mult_less_cancel_left [THEN iffD1], auto)
   done
 
 lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
@@ -1334,11 +1327,6 @@
 qed
 
 
-subsection {* Simproc setup *}
-
-use "Tools/int_factor_simprocs.ML"
-
-
 subsection {* Code generation *}
 
 definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where