# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1493206892 -7200
# Node ID baf96277ee7624fa5f0e739dadc9600731469dab
# Parent  66351f79c295db0335a26311c696e212119cd0cd
better code equation for binomial

diff -r 66351f79c295 -r baf96277ee76 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Binomial.thy	Wed Apr 26 13:41:32 2017 +0200
@@ -1688,10 +1688,8 @@
     (simp_all add: gbinomial_prod_rev prod_atLeastAtMost_code [symmetric]
       atLeastLessThanSuc_atLeastAtMost)
 
-(* FIXME *)
-(*TODO: This code equation breaks Scala code generation in HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)
-
-(*
+lemmas [code del] = binomial_Suc_Suc binomial_n_0 binomial_0_Suc
+    
 lemma binomial_code [code]:
   "(n choose k) =
       (if k > n then 0
@@ -1702,10 +1700,9 @@
     assume "k \<le> n"
     then have "{1..n} = {1..n-k} \<union> {n-k+1..n}" by auto
     then have "(fact n :: nat) = fact (n-k) * \<Prod>{n-k+1..n}"
-      by (simp add: prod.union_disjoint fact_altdef_nat)
+      by (simp add: prod.union_disjoint fact_prod)
   }
   then show ?thesis by (auto simp: binomial_altdef_nat mult_ac prod_atLeastAtMost_code)
 qed
-*)
 
 end