src/HOL/Codatatype/BNF_GFP.thy
changeset 49328 a1c10b46fecd
parent 49325 340844cbf7af
child 49509 163914705f8d
     1.1 --- a/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 11:38:22 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 11:39:05 2012 +0200
     1.3 @@ -321,9 +321,6 @@
     1.4  lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
     1.5  by auto
     1.6  
     1.7 -lemma sum_case_cong: "p = q \<Longrightarrow> sum_case f g p = sum_case f g q"
     1.8 -by simp
     1.9 -
    1.10  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
    1.11  by simp
    1.12