--- a/src/HOL/Lattices.thy Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Lattices.thy Mon Jul 12 10:48:37 2010 +0200
@@ -623,10 +623,10 @@
begin
definition
- inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
+ inf_fun_eq: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
definition
- sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
+ sup_fun_eq: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
instance proof
qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)