src/HOL/BNF/BNF_FP_Base.thy

--- a/src/HOL/BNF/BNF_FP_Base.thy	Wed Sep 25 21:25:53 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Thu Sep 26 01:05:06 2013 +0200
@@ -13,6 +13,9 @@
 imports BNF_Comp BNF_Ctr_Sugar
 begin
 
+lemma not_TrueE: "\<not> True \<Longrightarrow> P"
+by (erule notE, rule TrueI)
+
 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
 by auto
 
@@ -162,16 +165,6 @@
 lemma eq_ifI: "\<lbrakk>b \<Longrightarrow> t = x; \<not> b \<Longrightarrow> t = y\<rbrakk> \<Longrightarrow> t = (if b then x else y)"
   by fastforce
 
-lemma if_if_True:
-  "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
-   (if b then x else if b' then x' else f y')"
-  by simp
-
-lemma if_if_False:
-  "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
-   (if b then f y else if b' then x' else f y')"
-  by simp
-
 ML_file "Tools/bnf_fp_util.ML"
 ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/bnf_fp_def_sugar.ML"