src/HOLCF/Ffun.thy

--- a/src/HOLCF/Ffun.thy	Thu Jan 31 21:22:03 2008 +0100
+++ b/src/HOLCF/Ffun.thy	Thu Jan 31 21:23:14 2008 +0100
@@ -98,6 +98,14 @@
 
 instance "fun" :: (finite, finite_po) finite_po ..
 
+instance "fun" :: (type, discrete_cpo) discrete_cpo
+proof
+  fix f g :: "'a \<Rightarrow> 'b"
+  show "f \<sqsubseteq> g \<longleftrightarrow> f = g" 
+    unfolding expand_fun_less expand_fun_eq
+    by simp
+qed
+
 text {* chain-finite function spaces *}
 
 lemma maxinch2maxinch_lambda: