diff -r 46f59511b7bb -r d97fdabd9e2b src/Sequents/ILL_predlog.thy
--- a/src/Sequents/ILL_predlog.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/Sequents/ILL_predlog.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -5,16 +5,16 @@
 typedecl plf
 
 consts
-  conj :: "[plf,plf] \<Rightarrow> plf"   (infixr "&" 35)
-  disj :: "[plf,plf] \<Rightarrow> plf"   (infixr "|" 35)
-  impl :: "[plf,plf] \<Rightarrow> plf"   (infixr ">" 35)
-  eq :: "[plf,plf] \<Rightarrow> plf"   (infixr "=" 35)
-  ff :: "plf"    ("ff")
+  conj :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>&\<close> 35)
+  disj :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>|\<close> 35)
+  impl :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>>\<close> 35)
+  eq :: "[plf,plf] \<Rightarrow> plf"   (infixr \<open>=\<close> 35)
+  ff :: "plf"    (\<open>ff\<close>)
 
-  PL    :: "plf \<Rightarrow> o"      ("[* / _ / *]" [] 100)
+  PL    :: "plf \<Rightarrow> o"      (\<open>[* / _ / *]\<close> [] 100)
 
 syntax
-  "_NG" :: "plf \<Rightarrow> plf"   ("- _ " [50] 55)
+  "_NG" :: "plf \<Rightarrow> plf"   (\<open>- _ \<close> [50] 55)
 
 translations
   "[* A & B *]" \<rightleftharpoons> "[*A*] && [*B*]"