src/HOL/Lattices.thy
changeset 37767 a2b7a20d6ea3
parent 36673 6d25e8dab1e3
child 41075 4bed56dc95fb
     1.1 --- a/src/HOL/Lattices.thy	Mon Jul 12 08:58:27 2010 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Mon Jul 12 10:48:37 2010 +0200
     1.3 @@ -623,10 +623,10 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  inf_fun_eq [code del]: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
     1.8 +  inf_fun_eq: "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
     1.9  
    1.10  definition
    1.11 -  sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    1.12 +  sup_fun_eq: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    1.13  
    1.14  instance proof
    1.15  qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)