src/HOL/HOLCF/Ssum.thy
 changeset 45695 b108b3d7c49e parent 44066 d74182c93f04 child 46125 00cd193a48dc
```     1.1 --- a/src/HOL/HOLCF/Ssum.thy	Wed Nov 30 16:27:10 2011 +0100
1.2 +++ b/src/HOL/HOLCF/Ssum.thy	Wed Nov 30 17:30:01 2011 +0100
1.3 @@ -13,11 +13,14 @@
1.4
1.5  subsection {* Definition of strict sum type *}
1.6
1.7 -pcpodef ('a, 'b) ssum (infixr "++" 10) =
1.8 -  "{p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
1.9 -    (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
1.10 -    (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>) }"
1.11 -by simp_all
1.12 +definition
1.13 +  "ssum =
1.14 +    {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
1.15 +      (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
1.16 +      (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
1.17 +
1.18 +pcpodef (open) ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
1.19 +  unfolding ssum_def by simp_all
1.20
1.21  instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
1.22  by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])
```