src/HOL/Fact.thy
changeset 30082 43c5b7bfc791
parent 30073 a4ad0c08b7d9
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Fact.thy	Tue Feb 24 11:10:05 2009 -0800
     1.2 +++ b/src/HOL/Fact.thy	Tue Feb 24 11:12:58 2009 -0800
     1.3 @@ -58,7 +58,7 @@
     1.4    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
     1.5  apply (induct n arbitrary: m)
     1.6  apply auto
     1.7 -apply (drule_tac x = "m - 1" in meta_spec, auto)
     1.8 +apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
     1.9  done
    1.10  
    1.11  lemma fact_num0: "fact 0 = 1"