1.1 --- a/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 19 01:15:26 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 19 02:30:45 2013 +0200
     1.3 @@ -172,6 +172,15 @@
     1.4     (if b then f y else if b' then x' else f y')"
     1.5    by simp
     1.6  
     1.7 +lemma if_then_else_True_False:
     1.8 +  "(if p then False else r) \<longleftrightarrow> \<not> p \<and> r"
     1.9 +  "(if p then True else r) \<longleftrightarrow> p \<or> r"
    1.10 +  "(if p then q else False) \<longleftrightarrow> p \<and> q"
    1.11 +  "(if p then q else True) \<longleftrightarrow> \<not> p \<or> q"
    1.12 +by simp_all
    1.13 +
    1.14 +lemmas bool_if_simps = bool_simps(7,8,15-17,19,21-24,29-32) if_then_else_True_False
    1.15 +
    1.16  ML_file "Tools/bnf_fp_util.ML"
    1.17  ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
    1.18  ML_file "Tools/bnf_fp_def_sugar.ML"