# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1426605085 0
# Node ID cd945dc13becbb37f6477d43d2296ac3dbefcaec
# Parent  f13bb49dba085845fd71cc6755fcf810ba84aed3
more general type class for factorial. Now allows code generation (?)

diff -r f13bb49dba08 -r cd945dc13bec src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Tue Mar 17 14:16:16 2015 +0000
+++ b/src/HOL/Binomial.thy	Tue Mar 17 15:11:25 2015 +0000
@@ -13,7 +13,7 @@
 
 subsection {* Factorial *}
 
-fun fact :: "nat \<Rightarrow> ('a::{semiring_char_0,semiring_no_zero_divisors})"
+fun fact :: "nat \<Rightarrow> ('a::semiring_char_0)"
   where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
 
 lemmas fact_Suc = fact.simps(2)
@@ -30,7 +30,7 @@
 lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
   by (cases n) auto
 
-lemma fact_nonzero [simp]: "fact n \<noteq> 0"
+lemma fact_nonzero [simp]: "fact n \<noteq> (0::'a::{semiring_char_0,semiring_no_zero_divisors})"
   apply (induct n)
   apply auto
   using of_nat_eq_0_iff by fastforce
diff -r f13bb49dba08 -r cd945dc13bec src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Tue Mar 17 14:16:16 2015 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Tue Mar 17 15:11:25 2015 +0000
@@ -28,13 +28,6 @@
 
 code_pred sublist .
 
-lemma [code]:  -- {* for the generic factorial function *}
-  fixes XXX :: "'a :: semiring_numeral_div"
-  shows
-   "fact 0       = (1 :: 'a)"
-   "fact (Suc n) = (of_nat (Suc n) * fact n :: 'a)"
- by simp_all
-
 code_reserved SML upto -- {* avoid popular infix *}
 
 end