src/HOL/Fact.thy
 changeset 32047 c141f139ce26 parent 32039 400a519bc888 child 32558 e6e1fc2e73cb
```     1.1 --- a/src/HOL/Fact.thy	Fri Jul 17 10:07:15 2009 +0200
1.2 +++ b/src/HOL/Fact.thy	Fri Jul 17 13:12:18 2009 -0400
1.3 @@ -24,7 +24,7 @@
1.4    fact_nat :: "nat \<Rightarrow> nat"
1.5  where
1.6    fact_0_nat: "fact_nat 0 = Suc 0"
1.7 -| fact_Suc_nat: "fact_nat (Suc x) = Suc x * fact x"
1.8 +| fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
1.9
1.10  instance proof qed
1.11
1.12 @@ -100,7 +100,7 @@
1.13  lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
1.14    apply (subgoal_tac "n = Suc (n - 1)")
1.15    apply (erule ssubst)
1.16 -  apply (subst fact_Suc_nat)
1.17 +  apply (subst fact_Suc)
1.18    apply simp_all
1.19  done
1.20
1.21 @@ -142,7 +142,7 @@
1.22  lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
1.23    apply (induct n)
1.24    apply force
1.25 -  apply (auto simp only: fact_Suc_nat)
1.26 +  apply (auto simp only: fact_Suc)
1.27    apply (subgoal_tac "m = Suc n")
1.28    apply (erule ssubst)
1.29    apply (rule dvd_triv_left)
1.30 @@ -170,7 +170,7 @@
1.31  lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
1.32    apply (induct n)
1.33    apply force
1.34 -  apply (subst fact_Suc_nat)
1.35 +  apply (subst fact_Suc)
1.36    apply (subst interval_Suc)
1.37    apply auto
1.38  done
```