# HG changeset patch
# User haftmann
# Date 1309640158 -7200
# Node ID 3f1a44c2d64554f5a00e79dd84344cd7389df229
# Parent  905f17258bca0b7a38aa15c5bc3de3c9a3dfc449
install case certificate for If after code_datatype declaration for bool

diff -r 905f17258bca -r 3f1a44c2d645 src/HOL/HOL.thy
--- 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}
 *}
 
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 "==")