# HG changeset patch
# User nipkow
# Date 1362922578 -3600
# Node ID 1f5497c8ce8c3cb30724ed618e9ac4662916e9a7
# Parent  616f68ddcb7fa88fbab7a6faa23f63e4e5c78422# Parent  dbc4a77488b2c2cbf4f16c4172301f211014b8dc
merged

diff -r 616f68ddcb7f -r 1f5497c8ce8c src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Mar 10 11:21:16 2013 +0100
+++ b/src/HOL/Lattices.thy	Sun Mar 10 14:36:18 2013 +0100
@@ -649,17 +649,10 @@
 
 subsection {* Lattice on @{typ "_ \<Rightarrow> _"} *}
 
-instantiation "fun" :: (type, lattice) lattice
+instantiation "fun" :: (type, semilattice_sup) semilattice_sup
 begin
 
 definition
-  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
-
-lemma inf_apply [simp, code]:
-  "(f \<sqinter> g) x = f x \<sqinter> g x"
-  by (simp add: inf_fun_def)
-
-definition
   "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
 
 lemma sup_apply [simp, code]:
@@ -671,6 +664,23 @@
 
 end
 
+instantiation "fun" :: (type, semilattice_inf) semilattice_inf
+begin
+
+definition
+  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+
+lemma inf_apply [simp, code]:
+  "(f \<sqinter> g) x = f x \<sqinter> g x"
+  by (simp add: inf_fun_def)
+
+instance proof
+qed (simp_all add: le_fun_def)
+
+end
+
+instance "fun" :: (type, lattice) lattice ..
+
 instance "fun" :: (type, distrib_lattice) distrib_lattice proof
 qed (rule ext, simp add: sup_inf_distrib1)