--- a/src/HOL/BNF_Greatest_Fixpoint.thy Thu Apr 07 17:26:22 2016 +0200
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Thu Apr 07 17:56:22 2016 +0200
@@ -31,14 +31,6 @@
lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
by fast
-lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
- by (auto split: sum.splits)
-
-lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
- apply rule
- apply (rule ext, force split: sum.split)
- by (rule ext, metis case_sum_o_inj(2))
-
lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
by fast