src/HOL/Library/Convex.thy
changeset 57418 6ab1c7cb0b8d
parent 56796 9f84219715a7
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Library/Convex.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Library/Convex.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4      then have card: "card ({1 :: nat .. 2} \<inter> - {x. x = 1}) = 1"
     1.5        by simp
     1.6      then have "setsum ?u {1 .. 2} = 1"
     1.7 -      using setsum_cases[of "{(1 :: nat) .. 2}" "\<lambda> x. x = 1" "\<lambda> x. \<mu>" "\<lambda> x. 1 - \<mu>"]
     1.8 +      using setsum.If_cases[of "{(1 :: nat) .. 2}" "\<lambda> x. x = 1" "\<lambda> x. \<mu>" "\<lambda> x. 1 - \<mu>"]
     1.9        by auto
    1.10      with asm[rule_format, of "2" ?u ?x] have s: "(\<Sum>j \<in> {1..2}. ?u j *\<^sub>R ?x j) \<in> s"
    1.11        using mu xy by auto
    1.12 @@ -270,7 +270,7 @@
    1.13      by simp
    1.14    show "(\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s"
    1.15     using sum[THEN spec[where x="\<lambda>x. if x\<in>t then u x else 0"]] as *
    1.16 -   by (auto simp: assms setsum_cases if_distrib if_distrib_arg)
    1.17 +   by (auto simp: assms setsum.If_cases if_distrib if_distrib_arg)
    1.18  qed (erule_tac x=s in allE, erule_tac x=u in allE, auto)
    1.19  
    1.20