--- a/src/HOL/Algebra/Group.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Algebra/Group.thy Wed Jan 10 15:25:09 2018 +0100
@@ -676,7 +676,7 @@
(* Contributed by Joachim Breitner *)
lemma (in group) int_pow_is_hom:
- "x \<in> carrier G \<Longrightarrow> (op[^] x) \<in> hom \<lparr> carrier = UNIV, mult = op +, one = 0::int \<rparr> G "
+ "x \<in> carrier G \<Longrightarrow> (([^]) x) \<in> hom \<lparr> carrier = UNIV, mult = (+), one = 0::int \<rparr> G "
unfolding hom_def by (simp add: int_pow_mult)
@@ -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 = (=), le = (\<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 = (=), le = (\<subseteq>)\<rparr>"
(is "complete_lattice ?L")
proof (rule partial_order.complete_lattice_criterion1)
show "partial_order ?L" by (rule subgroups_partial_order)