Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
authorhuffman
Thu, 08 Dec 2011 13:46:04 +0100
changeset 45788 9049b24959de
parent 45787 9fcaf2557c59
child 45789 36ea69266e61
HOLCF/ex/Letrec.thy: keep class 'domain' as default sort
src/HOL/HOLCF/ex/Letrec.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOLCF/ex/Letrec.thy	Thu Dec 08 13:25:54 2011 +0100
+++ b/src/HOL/HOLCF/ex/Letrec.thy	Thu Dec 08 13:46:04 2011 +0100
@@ -8,10 +8,8 @@
 imports HOLCF
 begin
 
-default_sort pcpo
-
 definition
-  CLetrec :: "('a \<rightarrow> 'a \<times> 'b) \<rightarrow> 'b" where
+  CLetrec :: "('a::pcpo \<rightarrow> 'a \<times> 'b::pcpo) \<rightarrow> 'b" where
   "CLetrec = (\<Lambda> F. snd (F\<cdot>(\<mu> x. fst (F\<cdot>x))))"
 
 nonterminal recbinds and recbindt and recbind
isabelle