src/HOL/IntDiv.thy
 changeset 31065 d87465cbfc9e parent 30934 ed5377c2b0a3 child 31068 f591144b0f17
```     1.1 --- a/src/HOL/IntDiv.thy	Thu May 07 16:22:35 2009 +0200
1.2 +++ b/src/HOL/IntDiv.thy	Fri May 08 08:00:11 2009 +0200
1.3 @@ -8,10 +8,6 @@
1.4
1.5  theory IntDiv
1.6  imports Int Divides FunDef
1.7 -uses
1.8 -  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
1.9 -  "~~/src/Provers/Arith/extract_common_term.ML"
1.10 -  ("Tools/int_factor_simprocs.ML")
1.11  begin
1.12
1.13  definition divmod_rel :: "int \<Rightarrow> int \<Rightarrow> int \<times> int \<Rightarrow> bool" where
1.14 @@ -724,7 +720,6 @@
1.15        apply (auto simp add: divmod_rel_def)
1.16        apply (auto simp add: algebra_simps)
1.17        apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
1.18 -      apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
1.19        done
1.20      moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
1.21      ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
1.22 @@ -1078,8 +1073,6 @@
1.23     prefer 2
1.24     apply (blast intro: order_less_trans)
1.26 -  apply (subgoal_tac "n * k < n * 1")
1.27 -   apply (drule mult_less_cancel_left [THEN iffD1], auto)
1.28    done
1.29
1.30  lemma zmult_div_cancel: "(n::int) * (m div n) = m - (m mod n)"
1.31 @@ -1334,11 +1327,6 @@
1.32  qed
1.33
1.34
1.35 -subsection {* Simproc setup *}
1.36 -
1.37 -use "Tools/int_factor_simprocs.ML"
1.38 -
1.39 -
1.40  subsection {* Code generation *}
1.41
1.42  definition pdivmod :: "int \<Rightarrow> int \<Rightarrow> int \<times> int" where
```