# HG changeset patch
# User huffman
# Date 1117146242 -7200
# Node ID a92ee283393858fc1ef2d1fe69b2bfa4b9049f4a
# Parent  cdcbf5a7f38df350f06e43e196dae991db482adf
Use TypedefPcpo theorem for po instance

diff -r cdcbf5a7f38d -r a92ee2833938 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Fri May 27 00:16:18 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Fri May 27 00:24:02 2005 +0200
@@ -8,7 +8,7 @@
 header {* The type of continuous functions *}
 
 theory Cfun
-imports Cont
+imports TypedefPcpo
 begin
 
 defaultsort cpo
@@ -80,20 +80,8 @@
 defs (overloaded)
   less_cfun_def: "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )"
 
-lemma refl_less_cfun: "(f::'a->'b) << f"
-by (unfold less_cfun_def, rule refl_less)
-
-lemma antisym_less_cfun: 
-        "[|(f1::'a->'b) << f2; f2 << f1|] ==> f1 = f2"
-by (unfold less_cfun_def, rule Rep_CFun_inject[THEN iffD1], rule antisym_less)
-
-lemma trans_less_cfun: 
-        "[|(f1::'a->'b) << f2; f2 << f3|] ==> f1 << f3"
-by (unfold less_cfun_def, rule trans_less)
-
 instance "->" :: (cpo, cpo) po
-by intro_classes
-  (assumption | rule refl_less_cfun antisym_less_cfun trans_less_cfun)+
+by (rule typedef_po [OF type_definition_CFun less_cfun_def])
 
 text {* for compatibility with old HOLCF-Version *}
 lemma inst_cfun_po: "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)"