diff -r 905f17258bca -r 3f1a44c2d645 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Jul 02 22:14:47 2011 +0200
+++ b/src/HOL/Product_Type.thy	Sat Jul 02 22:55:58 2011 +0200
@@ -28,6 +28,15 @@
     and [code nbe]: "HOL.equal P P \<longleftrightarrow> True"
   by (simp_all add: equal)
 
+lemma If_case_cert:
+  assumes "CASE \<equiv> (\<lambda>b. If b f g)"
+  shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
+  using assms by simp_all
+
+setup {*
+  Code.add_case @{thm If_case_cert}
+*}
+
 code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   (Haskell infix 4 "==")