src/HOL/Code_Setup.thy
changeset 28699 32b6a8f12c1c
parent 28687 150a8a1eae1a
child 28740 22a8125d66fa
     1.1 --- a/src/HOL/Code_Setup.thy	Mon Oct 27 18:14:34 2008 +0100
     1.2 +++ b/src/HOL/Code_Setup.thy	Tue Oct 28 11:03:07 2008 +0100
     1.3 @@ -72,7 +72,7 @@
     1.4    using assms by simp_all
     1.5  
     1.6  lemma If_case_cert:
     1.7 -  includes meta_conjunction_syntax
     1.8 +  fixes meta_conjunction :: "prop => prop => prop"  (infixr "&&" 2)
     1.9    assumes "CASE \<equiv> (\<lambda>b. If b f g)"
    1.10    shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"
    1.11    using assms by simp_all