src/HOL/Product_Type.thy
changeset 43654 3f1a44c2d645
parent 43595 7ae4a23b5be6
child 43866 8a50dc70cbff
     1.1 --- a/src/HOL/Product_Type.thy	Sat Jul 02 22:14:47 2011 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Sat Jul 02 22:55:58 2011 +0200
     1.3 @@ -28,6 +28,15 @@
     1.4      and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
     1.5    by (simp_all add: equal)
     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 If_case_cert}
    1.14 +*}
    1.15 +
    1.16  code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.17    (Haskell infix 4 "==")
    1.18