Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOLCF/Sfun.thy
changeset 81583 b6df83045178
parent 80914 d97fdabd9e2b 
--- a/src/HOL/HOLCF/Sfun.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Sfun.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -8,7 +8,7 @@
   imports Cfun
 begin
 
-pcpodef ('a, 'b) sfun (infixr \<open>\<rightarrow>!\<close> 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
+pcpodef ('a::pcpo, 'b::pcpo) sfun (infixr \<open>\<rightarrow>!\<close> 0) = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
   by simp_all
 
 type_notation (ASCII)
@@ -16,10 +16,10 @@
 
 text \<open>TODO: Define nice syntax for abstraction, application.\<close>
 
-definition sfun_abs :: "('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow>! 'b)"
+definition sfun_abs :: "('a::pcpo \<rightarrow> 'b::pcpo) \<rightarrow> ('a \<rightarrow>! 'b)"
   where "sfun_abs = (\<Lambda> f. Abs_sfun (strictify\<cdot>f))"
 
-definition sfun_rep :: "('a \<rightarrow>! 'b) \<rightarrow> 'a \<rightarrow> 'b"
+definition sfun_rep :: "('a::pcpo \<rightarrow>! 'b::pcpo) \<rightarrow> 'a \<rightarrow> 'b"
   where "sfun_rep = (\<Lambda> f. Rep_sfun f)"
 
 lemma sfun_rep_beta: "sfun_rep\<cdot>f = Rep_sfun f"
isabelle