--- a/src/ZF/ex/BinEx.thy	Tue Sep 27 13:34:54 2022 +0200
+++ b/src/ZF/ex/BinEx.thy	Tue Sep 27 16:51:35 2022 +0100
@@ -23,7 +23,7 @@
 lemma "$- #65745 = #-65745"
 by simp (*80 msec*)
 
-(* negation of ~54321 *)
+(* negation of \<not>54321 *)
 lemma "$- #-54321 = #54321"
 by simp (*90 msec*)
 
@@ -62,7 +62,7 @@
 by simp
 
 
-(*** Quotient and remainder!! [they could be faster] ***)
+(*** Quotient and remainder\<And>[they could be faster] ***)
 
 lemma "#23 zdiv #3 = #7"
 by simp