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)