# HG changeset patch
# User huffman
# Date 1117060308 -7200
# Node ID defa6fa5fd29e54e6bc4fcbfa31931e498568f2b
# Parent  757e1c4a80814d04e6d86fc84710d63f5b73a849
removed dependence on Cfun.thy

diff -r 757e1c4a8081 -r defa6fa5fd29 src/HOLCF/TypedefPcpo.thy
--- a/src/HOLCF/TypedefPcpo.thy	Thu May 26 00:30:24 2005 +0200
+++ b/src/HOLCF/TypedefPcpo.thy	Thu May 26 00:31:48 2005 +0200
@@ -138,9 +138,6 @@
  apply (simp only: less type_definition.Abs_inverse [OF type f_in_A])
 done
 
-lemmas typedef_cont_Abs2 =
-  typedef_cont_Abs [OF _ _ _ _ cont_Rep_CFun2]
-
 
 subsection {* Proving a typedef is pointed *}