src/HOL/BNF_Greatest_Fixpoint.thy
changeset 62905 52c5a25e0c96
parent 61943 7fba644ed827
child 64413 c0d5e78eb647
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Apr 07 17:26:22 2016 +0200
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Thu Apr 07 17:56:22 2016 +0200
     1.3 @@ -31,14 +31,6 @@
     1.4  lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
     1.5    by fast
     1.6  
     1.7 -lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
     1.8 -  by (auto split: sum.splits)
     1.9 -
    1.10 -lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    1.11 -  apply rule
    1.12 -   apply (rule ext, force split: sum.split)
    1.13 -  by (rule ext, metis case_sum_o_inj(2))
    1.14 -
    1.15  lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
    1.16    by fast
    1.17