src/HOLCF/Cprod.thy
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