src/HOL/Lattices.thy

 lemma sup_apply [simp] (* CANDIDATE [code] *):
   "(f \<squnion> g) x = f x \<squnion> g x"
   by (simp add: sup_fun_def)
 
 instance proof
-qed (simp_all add: le_fun_def inf_apply sup_apply)
+qed (simp_all add: le_fun_def)
 
 end
 
 instance "fun" :: (type, distrib_lattice) distrib_lattice proof
-qed (rule ext, simp add: sup_inf_distrib1 inf_apply sup_apply)
+qed (rule ext, simp add: sup_inf_distrib1)
 
 instance "fun" :: (type, bounded_lattice) bounded_lattice ..
 
 instantiation "fun" :: (type, uminus) uminus
 begin

 instance ..
 
 end
 
 instance "fun" :: (type, boolean_algebra) boolean_algebra proof
-qed (rule ext, simp_all add: inf_apply sup_apply bot_apply top_apply uminus_apply minus_apply inf_compl_bot sup_compl_top diff_eq)+
+qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
 
 
 subsection {* Lattice on unary and binary predicates *}
 
 lemma inf1I: "A x \<Longrightarrow> B x \<Longrightarrow> (A \<sqinter> B) x"