src/HOL/Code_Setup.thy
changeset 28856 5e009a80fe6d
parent 28740 22a8125d66fa
child 29105 8f38bf68d42e
     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 {*