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