1.1 --- a/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 18 15:33:32 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 18 15:33:32 2013 +0200
     1.3 @@ -159,6 +159,9 @@
     1.4     (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
     1.5    unfolding Grp_def by rule auto
     1.6  
     1.7 +lemma eq_ifI: "\<lbrakk>b \<Longrightarrow> t = x; \<not> b \<Longrightarrow> t = y\<rbrakk> \<Longrightarrow> t = (if b then x else y)"
     1.8 +  by fastforce
     1.9 +
    1.10  lemma if_if_True:
    1.11    "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
    1.12     (if b then x else if b' then x' else f y')"