# HG changeset patch
# User haftmann
# Date 1204894382 -3600
# Node ID 3751b3dbb67c847da18886e46e94efe47c4453ee
# Parent  075264a0a4bcadb641e7a8e991e2c9ffcdbd7919
tuned proofs

diff -r 075264a0a4bc -r 3751b3dbb67c src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Mar 07 13:53:01 2008 +0100
+++ b/src/HOL/Lattices.thy	Fri Mar 07 13:53:02 2008 +0100
@@ -354,36 +354,10 @@
   unfolding Inf_Sup by auto
 
 lemma Inf_insert: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
-  apply (rule antisym)
-  apply (rule le_infI)
-  apply (rule Inf_lower)
-  apply simp
-  apply (rule Inf_greatest)
-  apply (rule Inf_lower)
-  apply simp
-  apply (rule Inf_greatest)
-  apply (erule insertE)
-  apply (rule le_infI1)
-  apply simp
-  apply (rule le_infI2)
-  apply (erule Inf_lower)
-  done
+  by (auto intro: antisym Inf_greatest Inf_lower)
 
 lemma Sup_insert: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
-  apply (rule antisym)
-  apply (rule Sup_least)
-  apply (erule insertE)
-  apply (rule le_supI1)
-  apply simp
-  apply (rule le_supI2)
-  apply (erule Sup_upper)
-  apply (rule le_supI)
-  apply (rule Sup_upper)
-  apply simp
-  apply (rule Sup_least)
-  apply (rule Sup_upper)
-  apply simp
-  done
+  by (auto intro: antisym Sup_least Sup_upper)
 
 lemma Inf_singleton [simp]:
   "\<Sqinter>{a} = a"