src/HOL/BNF_FP_Base.thy
changeset 57525 f9dd8a33f820
parent 57489 8f0ba9f2d10f
child 57641 dc59f147b27d
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Sat Jul 05 20:51:24 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Jul 07 16:06:46 2014 +0200
     1.3 @@ -13,6 +13,12 @@
     1.4  imports BNF_Comp Basic_BNFs
     1.5  begin
     1.6  
     1.7 +lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
     1.8 +  by default simp_all
     1.9 +
    1.10 +lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
    1.11 +  by default simp_all
    1.12 +
    1.13  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
    1.14  by auto
    1.15