--- a/src/HOL/Codatatype/BNF_Library.thy Mon Sep 10 17:36:02 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Library.thy Mon Sep 10 17:52:01 2012 +0200
@@ -829,6 +829,9 @@
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by simp
+lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
+by blast
+
lemma obj_sumE_f:
"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
by (metis sum.exhaust)