1.1 --- a/src/HOL/Code_Setup.thy Wed Nov 19 18:15:31 2008 +0100
1.2 +++ b/src/HOL/Code_Setup.thy Thu Nov 20 00:03:47 2008 +0100
1.3 @@ -78,9 +78,8 @@
1.4 using assms by simp_all
1.5
1.6 lemma If_case_cert:
1.7 - fixes meta_conjunction :: "prop => prop => prop" (infixr "&&" 2)
1.8 assumes "CASE \<equiv> (\<lambda>b. If b f g)"
1.9 - shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
1.10 + shows "(CASE True \<equiv> f) &&& (CASE False \<equiv> g)"
1.11 using assms by simp_all
1.12
1.13 setup {*