# HG changeset patch
# User nipkow
# Date 1515177176 -3600
# Node ID 7905adb28bdcf0fd31e70d9e4b8a99b87b1bacb2
# Parent  df79ef3b3a41d973ad02e70c130f56a5dd145f97
tuned op's

diff -r df79ef3b3a41 -r 7905adb28bdc src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Fri Jan 05 18:41:42 2018 +0100
+++ b/src/HOL/Algebra/Group.thy	Fri Jan 05 19:32:56 2018 +0100
@@ -773,7 +773,7 @@
 text_raw \<open>\label{sec:subgroup-lattice}\<close>
 
 theorem (in group) subgroups_partial_order:
-  "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
+  "partial_order \<lparr>carrier = {H. subgroup H G}, eq = op =, le = (op \<subseteq>)\<rparr>"
   by standard simp_all
 
 lemma (in group) subgroup_self:
@@ -818,7 +818,7 @@
 qed
 
 theorem (in group) subgroups_complete_lattice:
-  "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq>\<rparr>"
+  "complete_lattice \<lparr>carrier = {H. subgroup H G}, eq = op =, le = (op \<subseteq>)\<rparr>"
     (is "complete_lattice ?L")
 proof (rule partial_order.complete_lattice_criterion1)
   show "partial_order ?L" by (rule subgroups_partial_order)