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
```