--- a/src/HOL/HOLCF/Cpodef.thy Mon Dec 06 08:43:52 2010 -0800
+++ b/src/HOL/HOLCF/Cpodef.thy Mon Dec 06 08:59:58 2010 -0800
@@ -250,20 +250,6 @@
apply (simp add: type_definition.Rep_inject [OF type])
done
-theorem typedef_Abs_defined:
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and UU_in_A: "\<bottom> \<in> A"
- shows "\<lbrakk>x \<noteq> \<bottom>; x \<in> A\<rbrakk> \<Longrightarrow> Abs x \<noteq> \<bottom>"
-by (simp add: typedef_Abs_bottom_iff [OF type below UU_in_A])
-
-theorem typedef_Rep_defined:
- assumes type: "type_definition Rep Abs A"
- and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
- and UU_in_A: "\<bottom> \<in> A"
- shows "x \<noteq> \<bottom> \<Longrightarrow> Rep x \<noteq> \<bottom>"
-by (simp add: typedef_Rep_bottom_iff [OF type below UU_in_A])
-
subsection {* Proving a subtype is flat *}
theorem typedef_flat: