src/HOL/BNF_GFP.thy
changeset 55414 eab03e9cee8a
parent 55413 a8e96847523c
child 55415 05f5fdb8d093
     1.1 --- a/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -27,13 +27,13 @@
     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 sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
     1.8 +lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
     1.9  by (auto split: sum.splits)
    1.10  
    1.11 -lemma sum_case_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> sum_case g h = f"
    1.12 +lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    1.13  apply rule
    1.14   apply (rule ext, force split: sum.split)
    1.15 -by (rule ext, metis sum_case_o_inj(2))
    1.16 +by (rule ext, metis case_sum_o_inj(2))
    1.17  
    1.18  lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
    1.19  by fast