# HG changeset patch
# User eberlm
# Date 1452614372 -3600
# Node ID 18a217591310e0b395b62b2c36ed2ac99e2413a4
# Parent  00bfdf4bf23706d25ff6b4603e79d4a776a772c6
Deleted problematic code equation in Binomial temporarily.

diff -r 00bfdf4bf237 -r 18a217591310 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Tue Jan 12 15:23:54 2016 +0100
+++ b/src/HOL/Binomial.thy	Tue Jan 12 16:59:32 2016 +0100
@@ -1567,11 +1567,14 @@
      fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
   by (simp add: setprod_atLeastAtMost_code gbinomial_def)
 
+(*TODO: This code equation breaks Scala code generation in HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)
+
+(*
 lemma binomial_code [code]:
   "(n choose k) =
       (if k > n then 0
        else if 2 * k > n then (n choose (n - k))
-       else (fold_atLeastAtMost_nat (op *) (n-k+1) n 1 div fact k))"
+       else (fold_atLeastAtMost_nat (op * ) (n-k+1) n 1 div fact k))"
 proof -
   {
     assume "k \<le> n"
@@ -1581,5 +1584,6 @@
   }
   thus ?thesis by (auto simp: binomial_altdef_nat mult_ac setprod_atLeastAtMost_code)
 qed 
+*)
 
 end