# HG changeset patch
# User haftmann
# Date 1254323346 -7200
# Node ID be337ec31268ea670ff8b53700dea4d57f06e2da
# Parent  371c7f74282d7ddd71c5a3a5bcfc7a04592935ab
tuned proofs

diff -r 371c7f74282d -r be337ec31268 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Sep 30 17:04:21 2009 +0200
+++ b/src/HOL/Lattices.thy	Wed Sep 30 17:09:06 2009 +0200
@@ -547,21 +547,14 @@
 definition
   sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
 
-instance
-apply intro_classes
-unfolding inf_fun_eq sup_fun_eq
-apply (auto intro: le_funI)
-apply (rule le_funI)
-apply (auto dest: le_funD)
-apply (rule le_funI)
-apply (auto dest: le_funD)
-done
+instance proof
+qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)
 
 end
 
 instance "fun" :: (type, distrib_lattice) distrib_lattice
 proof
-qed (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
+qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
 
 instantiation "fun" :: (type, uminus) uminus
 begin