# HG changeset patch
# User wenzelm
# Date 1728555590 -7200
# Node ID 6e6766cddf734e86cba1eec1e3dd07ea8144b63e
# Parent  20ca8aa4b7ca365fb924ac5f5f5cf33ab6ec99ac
more syntax bundles;

diff -r 20ca8aa4b7ca -r 6e6766cddf73 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Oct 09 23:59:49 2024 +0200
+++ b/src/HOL/Algebra/Group.thy	Thu Oct 10 12:19:50 2024 +0200
@@ -21,10 +21,13 @@
   mult    :: "['a, 'a] \<Rightarrow> 'a" (infixl \<open>\<otimes>\<index>\<close> 70)
   one     :: 'a (\<open>\<one>\<index>\<close>)
 
-definition
-  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 m_inv :: "('a, 'b) monoid_scheme => 'a => 'a"
+  where "m_inv G 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>)"
+
+open_bundle m_inv_syntax
+begin
+notation m_inv  (\<open>(\<open>open_block notation=\<open>prefix inv\<close>\<close>inv\<index> _)\<close> [81] 80)
+end
 
 definition
   Units :: "_ => 'a set"