| changeset 36452 | d37c6eed8117 |
| parent 36176 | 3fe7e97ccca8 |
| child 36998 | 9316a18ec931 |
--- a/src/HOLCF/Fixrec.thy Wed Apr 28 11:41:27 2010 +0200 +++ b/src/HOLCF/Fixrec.thy Wed Apr 28 12:07:52 2010 +0200 @@ -13,7 +13,7 @@ subsection {* Maybe monad type *} -defaultsort cpo +default_sort cpo pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set" by simp_all @@ -463,7 +463,7 @@ subsection {* Match functions for built-in types *} -defaultsort pcpo +default_sort pcpo definition match_UU :: "'a \<rightarrow> 'c maybe \<rightarrow> 'c maybe"