# HG changeset patch
# User wenzelm
# Date 1322670601 -3600
# Node ID b108b3d7c49e14deebf371dfd364946ad269743b
# Parent  4a87436182570369604aa86ee28243f200806d42
prefer cpodef without extra definition;

diff -r 4a8743618257 -r b108b3d7c49e src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Wed Nov 30 16:27:10 2011 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Wed Nov 30 17:30:01 2011 +0100
@@ -13,8 +13,10 @@
 
 subsection {* Definition of continuous function type *}
 
-cpodef ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
-by (auto intro: cont_const adm_cont)
+definition "cfun = {f::'a => 'b. cont f}"
+
+cpodef (open) ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
+  unfolding cfun_def by (auto intro: cont_const adm_cont)
 
 type_notation (xsymbols)
   cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)
diff -r 4a8743618257 -r b108b3d7c49e src/HOL/HOLCF/Sprod.thy
--- a/src/HOL/HOLCF/Sprod.thy	Wed Nov 30 16:27:10 2011 +0100
+++ b/src/HOL/HOLCF/Sprod.thy	Wed Nov 30 17:30:01 2011 +0100
@@ -13,9 +13,10 @@
 
 subsection {* Definition of strict product type *}
 
-pcpodef ('a, 'b) sprod (infixr "**" 20) =
-        "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
-by simp_all
+definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
+
+pcpodef (open) ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set"
+  unfolding sprod_def by simp_all
 
 instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_sprod below_sprod_def])
diff -r 4a8743618257 -r b108b3d7c49e src/HOL/HOLCF/Ssum.thy
--- a/src/HOL/HOLCF/Ssum.thy	Wed Nov 30 16:27:10 2011 +0100
+++ b/src/HOL/HOLCF/Ssum.thy	Wed Nov 30 17:30:01 2011 +0100
@@ -13,11 +13,14 @@
 
 subsection {* Definition of strict sum type *}
 
-pcpodef ('a, 'b) ssum (infixr "++" 10) = 
-  "{p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
-    (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
-    (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>) }"
-by simp_all
+definition
+  "ssum =
+    {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
+      (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
+      (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
+
+pcpodef (open) ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+  unfolding ssum_def by simp_all
 
 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
 by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])