--- a/src/HOL/Algebra/Group.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Algebra/Group.thy Wed Oct 09 23:38:29 2024 +0200
@@ -22,7 +22,8 @@
one :: 'a (\<open>\<one>\<index>\<close>)
definition
- m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" (\<open>inv\<index> _\<close> [81] 80)
+ m_inv :: "('a, 'b) monoid_scheme => 'a => 'a"
+ (\<open>(\<open>open_block notation=\<open>prefix inv\<close>\<close>inv\<index> _)\<close> [81] 80)
where "inv\<^bsub>G\<^esub> x = (THE y. y \<in> carrier G \<and> x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> \<and> y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)"
definition