src/HOL/Fact.thy
changeset 30240 5b25fee0362c
parent 29693 708dcf7dec9f
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Fact.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Fact.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header{*Factorial Function*}
     1.5  
     1.6  theory Fact
     1.7 -imports Nat
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  consts fact :: "nat => nat"
    1.12 @@ -58,7 +58,7 @@
    1.13    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
    1.14  apply (induct n arbitrary: m)
    1.15  apply auto
    1.16 -apply (drule_tac x = "m - 1" in meta_spec, auto)
    1.17 +apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
    1.18  done
    1.19  
    1.20  lemma fact_num0: "fact 0 = 1"