diff -r 97f2ed240431 -r 2230b7047376 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Binomial.thy	Wed Feb 17 21:51:57 2016 +0100
@@ -25,9 +25,19 @@
 lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
   by simp
 
-lemma of_nat_fact [simp]: "of_nat (fact n) = fact n"
+lemma of_nat_fact [simp]:
+  "of_nat (fact n) = fact n"
   by (induct n) (auto simp add: algebra_simps of_nat_mult)
  
+lemma of_int_fact [simp]:
+  "of_int (fact n) = fact n"
+proof -
+  have "of_int (of_nat (fact n)) = fact n"
+    unfolding of_int_of_nat_eq by simp
+  then show ?thesis
+    by simp
+qed
+
 lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
   by (cases n) auto