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