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