--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:54 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:56 2014 +0200
@@ -189,14 +189,6 @@
"rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
unfolding rel_prod_def rel_fun_def convol_def by auto
-lemma Inl_transfer:
- "rel_fun S (rel_sum S T) Inl Inl"
- by auto
-
-lemma Inr_transfer:
- "rel_fun T (rel_sum S T) Inr Inr"
- by auto
-
lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
by (rule ssubst)