src/HOL/BNF_FP_Base.thy
changeset 57279 88263522c31e
parent 56846 9df717fef2bb
child 57301 7b997028aaac
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Wed Jun 18 17:42:24 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Wed Jun 18 17:42:24 2014 +0200
     1.3 @@ -71,9 +71,6 @@
     1.4  "case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
     1.5  by simp
     1.6  
     1.7 -lemma Inl_Inr_False: "(Inl x = Inr y) = False"
     1.8 -by simp
     1.9 -
    1.10  lemma prod_set_simps:
    1.11  "fsts (x, y) = {x}"
    1.12  "snds (x, y) = {y}"