src/HOLCF/Ffun.thy
changeset 20523 36a59e5d0039
parent 18291 4afdf02d9831
child 25758 89c7c22e64b4
     1.1 --- a/src/HOLCF/Ffun.thy	Wed Sep 13 00:38:38 2006 +0200
     1.2 +++ b/src/HOLCF/Ffun.thy	Wed Sep 13 12:05:50 2006 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  subsection {* Full function space is a partial order *}
     1.6  
     1.7 -instance fun  :: (type, sq_ord) sq_ord ..
     1.8 +instance "fun"  :: (type, sq_ord) sq_ord ..
     1.9  
    1.10  defs (overloaded)
    1.11    less_fun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x)"  
    1.12 @@ -36,7 +36,7 @@
    1.13  apply (erule spec)
    1.14  done
    1.15  
    1.16 -instance fun  :: (type, po) po
    1.17 +instance "fun"  :: (type, po) po
    1.18  by intro_classes
    1.19    (assumption | rule refl_less_fun antisym_less_fun trans_less_fun)+
    1.20  
    1.21 @@ -90,7 +90,7 @@
    1.22    "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
    1.23  by (rule exI, erule lub_fun)
    1.24  
    1.25 -instance fun  :: (type, cpo) cpo
    1.26 +instance "fun"  :: (type, cpo) cpo
    1.27  by intro_classes (rule cpo_fun)
    1.28  
    1.29  subsection {* Full function space is pointed *}
    1.30 @@ -103,7 +103,7 @@
    1.31  apply (rule minimal_fun [THEN allI])
    1.32  done
    1.33  
    1.34 -instance fun  :: (type, pcpo) pcpo
    1.35 +instance "fun"  :: (type, pcpo) pcpo
    1.36  by intro_classes (rule least_fun)
    1.37  
    1.38  text {* for compatibility with old HOLCF-Version *}