| changeset 57471 | 11cd462e31ec |
| parent 57303 | 498a62e65f5f |
| child 57489 | 8f0ba9f2d10f |
--- a/src/HOL/BNF_FP_Base.thy Tue Jul 01 16:26:14 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Tue Jul 01 17:01:28 2014 +0200 @@ -89,6 +89,9 @@ lemma Inl_Inr_False: "(Inl x = Inr y) = False" by simp +lemma Inr_Inl_False: "(Inr x = Inl y) = False" + by simp + lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y" by blast