# HG changeset patch
# User huffman
# Date 1133308561 -3600
# Node ID 4afdf02d9831007c13fba641308eb71c46c98dd0
# Parent  5fc3097708402d6ef066ab84eb9de339a259ab1a
changed section names

diff -r 5fc309770840 -r 4afdf02d9831 src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Wed Nov 30 00:55:24 2005 +0100
+++ b/src/HOLCF/Ffun.thy	Wed Nov 30 00:56:01 2005 +0100
@@ -13,7 +13,7 @@
 imports Pcpo
 begin
 
-subsection {* Type @{typ "'a => 'b"} is a partial order *}
+subsection {* Full function space is a partial order *}
 
 instance fun  :: (type, sq_ord) sq_ord ..
 
@@ -48,7 +48,7 @@
 lemma less_fun_ext: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> g"
 by (simp add: less_fun_def)
 
-subsection {* Type @{typ "'a::type => 'b::cpo"} is chain complete *}
+subsection {* Full function space is chain complete *}
 
 text {* chains of functions yield chains in the po range *}
 
@@ -93,7 +93,7 @@
 instance fun  :: (type, cpo) cpo
 by intro_classes (rule cpo_fun)
 
-subsection {* Type @{typ "'a::type => 'b::pcpo"} is pointed *}
+subsection {* Full function space is pointed *}
 
 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f"
 by (simp add: less_fun_def)