--- a/src/ZF/ex/Ring.thy	Tue Oct 08 15:02:17 2024 +0200
+++ b/src/ZF/ex/Ring.thy	Tue Oct 08 15:44:11 2024 +0200
@@ -6,9 +6,7 @@
 
 theory Ring imports Group begin
 
-no_notation
-  cadd  (infixl \<open>\<oplus>\<close> 65) and
-  cmult  (infixl \<open>\<otimes>\<close> 70)
+no_notation cadd  (infixl \<open>\<oplus>\<close> 65) and cmult  (infixl \<open>\<otimes>\<close> 70)
 
 (*First, we must simulate a record declaration:
 record ring = monoid +