diff -r 8758895ea413 -r aa5dfb03eb1e src/HOLCF/Cprod.thy --- 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 \ unit \ 'a" where