src/HOL/BNF_FP_Base.thy
changeset 57301 7b997028aaac
parent 57279 88263522c31e
child 57302 58f02fbaa764
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Tue Jun 24 12:36:45 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Tue Jun 24 13:48:14 2014 +0200
     1.3 @@ -83,6 +83,9 @@
     1.4  "setr (Inr x) = {x}"
     1.5  unfolding sum_set_defs by simp+
     1.6  
     1.7 +lemma Inl_Inr_False: "(Inl x = Inr 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