# HG changeset patch
# User wenzelm
# Date 1314220805 -7200
# Node ID 6f2943e34d60caedd9165b4c1167c27d2cdf5ddd
# Parent  3c2b2c4a7c1cb15daa1484a71e887bac286e526e
tuned proofs;

diff -r 3c2b2c4a7c1c -r 6f2943e34d60 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Aug 24 23:19:40 2011 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed Aug 24 23:20:05 2011 +0200
@@ -154,7 +154,7 @@
     and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
   then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
     by (simp add: m_assoc Units_closed del: Units_l_inv)
-  with G show "y = z" by (simp add: Units_l_inv)
+  with G show "y = z" by simp
 next
   assume eq: "y = z"
     and G: "x \<in> Units G"  "y \<in> carrier G"  "z \<in> carrier G"
@@ -332,7 +332,7 @@
 proof -
   assume x: "x \<in> carrier G"
   then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
-    by (simp add: m_assoc [symmetric] l_inv)
+    by (simp add: m_assoc [symmetric])
   with x show ?thesis by (simp del: r_one)
 qed
 
@@ -372,7 +372,7 @@
 proof -
   assume G: "x \<in> carrier G"  "y \<in> carrier G"
   then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
-    by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
+    by (simp add: m_assoc) (simp add: m_assoc [symmetric])
   with G show ?thesis by (simp del: l_inv Units_l_inv)
 qed
 
@@ -446,7 +446,7 @@
 lemma (in group) one_in_subset:
   "[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
    ==> \<one> \<in> H"
-by (force simp add: l_inv)
+by force
 
 text {* A characterization of subgroups: closed, non-empty subset. *}
 
diff -r 3c2b2c4a7c1c -r 6f2943e34d60 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Wed Aug 24 23:19:40 2011 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Wed Aug 24 23:20:05 2011 +0200
@@ -34,7 +34,8 @@
 
 subsubsection {* The order relation *}
 
-context weak_partial_order begin
+context weak_partial_order
+begin
 
 lemma le_cong_l [intro, trans]:
   "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
@@ -85,7 +86,7 @@
     and  yy': "y .= y'"
     and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   shows "x \<sqsubset> y'"
-  using assms unfolding lless_def by (auto intro: trans sym)
+  using assms unfolding lless_def by (auto intro: trans sym)  (*slow*)
 
 
 lemma (in weak_partial_order) lless_antisym:
@@ -574,8 +575,7 @@
   proof (cases "A = {}")
     case True
     with insert show ?thesis
-      by simp (simp add: least_cong [OF weak_sup_of_singleton]
-        sup_of_singleton_closed sup_of_singletonI)
+      by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI)
         (* The above step is hairy; least_cong can make simp loop.
         Would want special version of simp to apply least_cong. *)
   next
@@ -1282,7 +1282,7 @@
   (is "complete_lattice ?L")
 proof (rule partial_order.complete_latticeI)
   show "partial_order ?L"
-    proof qed auto
+    by default auto
 next
   fix B
   assume B: "B \<subseteq> carrier ?L"