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