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/HOLCF/Fun_Cpo.thy
changeset 40089 8adc57fb8454
parent 40011 b974cf829099
child 40091 1ca61fbd8a79 
--- a/src/HOLCF/Fun_Cpo.thy	Fri Oct 22 06:08:51 2010 -0700
+++ b/src/HOLCF/Fun_Cpo.thy	Fri Oct 22 06:58:45 2010 -0700
@@ -128,8 +128,6 @@
   thus "\<exists>n. max_in_chain n Y" ..
 qed
 
-instance "fun" :: (finite, finite_po) finite_po ..
-
 instance "fun" :: (type, discrete_cpo) discrete_cpo
 proof
   fix f g :: "'a \<Rightarrow> 'b"
isabelle