# HG changeset patch
# User huffman
# Date 1288394647 25200
# Node ID 24971566ff4f44f472f5c5cafeb0c6941856d943
# Parent  b5e1ab22198aeb059a381b10c333fa9d15db8caa
simplify proof of typedef_cont_Abs

diff -r b5e1ab22198a -r 24971566ff4f src/HOLCF/Pcpodef.thy
--- a/src/HOLCF/Pcpodef.thy	Wed Oct 27 15:50:01 2010 -0700
+++ b/src/HOLCF/Pcpodef.thy	Fri Oct 29 16:24:07 2010 -0700
@@ -152,13 +152,9 @@
     and below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     and adm: "adm (\<lambda>x. x \<in> A)" (* not used *)
     and f_in_A: "\<And>x. f x \<in> A"
-    and cont_f: "cont f"
-  shows "cont (\<lambda>x. Abs (f x))"
- apply (rule contI)
- apply (rule typedef_is_lubI [OF below])
- apply (simp only: type_definition.Abs_inverse [OF type f_in_A])
- apply (erule cont_f [THEN contE])
-done
+  shows "cont f \<Longrightarrow> cont (\<lambda>x. Abs (f x))"
+unfolding cont_def is_lub_def is_ub_def ball_simps below
+by (simp add: type_definition.Abs_inverse [OF type f_in_A])
 
 subsection {* Proving subtype elements are compact *}