src/HOL/BNF_FP_Base.thy
changeset 57303 498a62e65f5f
parent 57302 58f02fbaa764
child 57471 11cd462e31ec
     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,7 +16,7 @@
     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 +lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
     1.9    by auto
    1.10  
    1.11  lemma eq_sym_Unity_conv: "(x = (() = ())) = x"