--- a/src/HOL/HOL.thy Sat Jul 02 22:14:47 2011 +0200
+++ b/src/HOL/HOL.thy Sat Jul 02 22:55:58 2011 +0200
@@ -1892,14 +1892,8 @@
shows "CASE x \<equiv> f x"
using assms by simp_all
-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 Let_case_cert}
- #> Code.add_case @{thm If_case_cert}
#> Code.add_undefined @{const_name undefined}
*}
--- 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 "==")