src/HOL/Groups.thy

--- a/src/HOL/Groups.thy	Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Groups.thy	Tue Oct 08 12:10:35 2024 +0200
@@ -198,11 +198,16 @@
   fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl \<open>-\<close> 65)
 
 class uminus =
-  fixes uminus :: "'a \<Rightarrow> 'a"  (\<open>- _\<close> [81] 80)
+  fixes uminus :: "'a \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>prefix -\<close>\<close>- _)\<close> [81] 80)
 
 class times =
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl \<open>*\<close> 70)
 
+bundle uminus_syntax
+begin
+notation uminus  (\<open>(\<open>open_block notation=\<open>prefix -\<close>\<close>- _)\<close> [81] 80)
+end
+
 
 subsection \<open>Semigroups and Monoids\<close>
 
@@ -1164,7 +1169,12 @@
 end
 
 class abs =
-  fixes abs :: "'a \<Rightarrow> 'a"  (\<open>\<bar>_\<bar>\<close>)
+  fixes abs :: "'a \<Rightarrow> 'a"  (\<open>(\<open>open_block notation=\<open>mixfix abs\<close>\<close>\<bar>_\<bar>)\<close>)
+
+bundle abs_syntax
+begin
+notation abs  (\<open>(\<open>open_block notation=\<open>mixfix abs\<close>\<close>\<bar>_\<bar>)\<close>)
+end
 
 class sgn =
   fixes sgn :: "'a \<Rightarrow> 'a"