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