changeset 35900 | aa5dfb03eb1e |
parent 33399 | 768b2bb9e66a |
child 35922 | bfa52a972745 |
--- a/src/HOLCF/Cprod.thy Mon Mar 22 19:29:11 2010 +0100 +++ b/src/HOLCF/Cprod.thy Mon Mar 22 12:52:51 2010 -0700 @@ -10,7 +10,7 @@ defaultsort cpo -subsection {* Type @{typ unit} is a pcpo *} +subsection {* Continuous case function for unit type *} definition unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a" where