--- 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. *}
--- 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"