src/HOL/BNF_FP_Base.thy
changeset 57302 58f02fbaa764
parent 57301 7b997028aaac
child 57303 498a62e65f5f
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Tue Jun 24 13:48:14 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Tue Jun 24 13:48:14 2014 +0200
     1.3 @@ -16,6 +16,9 @@
     1.4  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
     1.5  by auto
     1.6  
     1.7 +lemma predicate2D_conj: "(P \<le> Q) \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
     1.8 +  by auto
     1.9 +
    1.10  lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
    1.11  by blast
    1.12