tuned proofs
authorhaftmann
Wed Sep 30 17:09:06 2009 +0200 (2009-09-30)
changeset 32780be337ec31268
parent 32779 371c7f74282d
child 32781 19c01bd7f6ae
tuned proofs
src/HOL/Lattices.thy
     1.1 --- a/src/HOL/Lattices.thy	Wed Sep 30 17:04:21 2009 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Wed Sep 30 17:09:06 2009 +0200
     1.3 @@ -547,21 +547,14 @@
     1.4  definition
     1.5    sup_fun_eq [code del]: "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
     1.6  
     1.7 -instance
     1.8 -apply intro_classes
     1.9 -unfolding inf_fun_eq sup_fun_eq
    1.10 -apply (auto intro: le_funI)
    1.11 -apply (rule le_funI)
    1.12 -apply (auto dest: le_funD)
    1.13 -apply (rule le_funI)
    1.14 -apply (auto dest: le_funD)
    1.15 -done
    1.16 +instance proof
    1.17 +qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq)
    1.18  
    1.19  end
    1.20  
    1.21  instance "fun" :: (type, distrib_lattice) distrib_lattice
    1.22  proof
    1.23 -qed (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
    1.24 +qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1)
    1.25  
    1.26  instantiation "fun" :: (type, uminus) uminus
    1.27  begin