src/HOL/Algebra/Group.thy
 changeset 27713 95b36bfe7fc4 parent 27698 197f0517f0bd child 27714 27b4d7c01f8b
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Jul 30 16:07:00 2008 +0200
1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Jul 30 19:03:33 2008 +0200
1.3 @@ -712,8 +712,8 @@
1.4  text_raw {* \label{sec:subgroup-lattice} *}
1.5
1.6  theorem (in group) subgroups_partial_order:
1.7 -  "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
1.8 -  by (rule partial_order.intro) simp_all
1.9 +  "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
1.10 +  by unfold_locales simp_all
1.11
1.12  lemma (in group) subgroup_self:
1.13    "subgroup (carrier G) G"
1.14 @@ -757,7 +757,7 @@
1.15  qed
1.16
1.17  theorem (in group) subgroups_complete_lattice:
1.18 -  "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
1.19 +  "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
1.20      (is "complete_lattice ?L")
1.21  proof (rule partial_order.complete_lattice_criterion1)
1.22    show "partial_order ?L" by (rule subgroups_partial_order)