# HG changeset patch
# User nipkow
# Date 1402310182 -7200
# Node ID 4cf607675df8190b2d4975a25642ed5d63e185db
# Parent  d9a18e44b80d8f8604343bebf0df3096aa67a59b
Sup/Inf on functions decoupled from complete_lattice.

diff -r d9a18e44b80d -r 4cf607675df8 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sun Jun 08 23:30:53 2014 +0200
+++ b/src/HOL/Complete_Lattices.thy	Mon Jun 09 12:36:22 2014 +0200
@@ -719,7 +719,7 @@
 
 subsection {* Complete lattice on @{typ "_ \<Rightarrow> _"} *}
 
-instantiation "fun" :: (type, complete_lattice) complete_lattice
+instantiation "fun" :: (type, Inf) Inf
 begin
 
 definition
@@ -729,6 +729,13 @@
   "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   by (simp add: Inf_fun_def)
 
+instance ..
+
+end
+
+instantiation "fun" :: (type, Sup) Sup
+begin
+
 definition
   "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
 
@@ -736,6 +743,13 @@
   "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   by (simp add: Sup_fun_def)
 
+instance ..
+
+end
+
+instantiation "fun" :: (type, complete_lattice) complete_lattice
+begin
+
 instance proof
 qed (auto simp add: le_fun_def intro: INF_lower INF_greatest SUP_upper SUP_least)