src/HOL/Fact.thy
changeset 46240 933f35c4e126
parent 45930 2a882ef2cd73
child 50224 aacd6da09825
     1.1 --- a/src/HOL/Fact.thy	Tue Jan 17 11:15:36 2012 +0100
     1.2 +++ b/src/HOL/Fact.thy	Tue Jan 17 16:30:54 2012 +0100
     1.3 @@ -255,8 +255,6 @@
     1.4      fact m < fact ((m + 1) + k)"
     1.5    apply (induct k rule: int_ge_induct)
     1.6    apply (simp add: fact_plus_one_int)
     1.7 -  apply (subst mult_less_cancel_right1)
     1.8 -  apply (insert fact_gt_zero_int [of m], arith)
     1.9    apply (subst (2) fact_reduce_int)
    1.10    apply (auto simp add: add_ac)
    1.11    apply (erule order_less_le_trans)