diff -r 6ce0c8d59f5a -r ec121999a9cb 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 \ 'a \ 'a" (infixl \-\ 65) class uminus = - fixes uminus :: "'a \ 'a" (\- _\ [81] 80) + fixes uminus :: "'a \ 'a" (\(\open_block notation=\prefix -\\- _)\ [81] 80) class times = fixes times :: "'a \ 'a \ 'a" (infixl \*\ 70) +bundle uminus_syntax +begin +notation uminus (\(\open_block notation=\prefix -\\- _)\ [81] 80) +end + subsection \Semigroups and Monoids\ @@ -1164,7 +1169,12 @@ end class abs = - fixes abs :: "'a \ 'a" (\\_\\) + fixes abs :: "'a \ 'a" (\(\open_block notation=\mixfix abs\\\_\)\) + +bundle abs_syntax +begin +notation abs (\(\open_block notation=\mixfix abs\\\_\)\) +end class sgn = fixes sgn :: "'a \ 'a"