src/HOL/HOL.thy
changeset 43654 3f1a44c2d645
parent 43597 b4a093e755db
child 44021 7c39c83002b9
     1.1 --- a/src/HOL/HOL.thy	Sat Jul 02 22:14:47 2011 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Jul 02 22:55:58 2011 +0200
     1.3 @@ -1892,14 +1892,8 @@
     1.4    shows "CASE x \<equiv> f x"
     1.5    using assms by simp_all
     1.6  
     1.7 -lemma If_case_cert:
     1.8 -  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
     1.9 -  shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
    1.10 -  using assms by simp_all
    1.11 -
    1.12  setup {*
    1.13    Code.add_case @{thm Let_case_cert}
    1.14 -  #> Code.add_case @{thm If_case_cert}
    1.15    #> Code.add_undefined @{const_name undefined}
    1.16  *}
    1.17