changeset 36452 | d37c6eed8117 |
parent 35933 | f135ebcc835c |
child 37079 | 0cd15d8c90a0 |
--- a/src/HOLCF/Cfun.thy Wed Apr 28 11:41:27 2010 +0200 +++ b/src/HOLCF/Cfun.thy Wed Apr 28 12:07:52 2010 +0200 @@ -9,7 +9,7 @@ imports Pcpodef Ffun Product_Cpo begin -defaultsort cpo +default_sort cpo subsection {* Definition of continuous function type *} @@ -511,7 +511,7 @@ subsection {* Strictified functions *} -defaultsort pcpo +default_sort pcpo definition strictify :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where