diff -r 01b8c8d17f13 -r 2a77bc3b4eac src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Fri Sep 20 23:36:33 2024 +0200
+++ b/src/Sequents/ILL.thy	Fri Sep 20 23:37:00 2024 +0200
@@ -29,8 +29,8 @@
   PromAux :: "three_seqi"
 
 syntax
-  "_Trueprop" :: "single_seqe" (\<open>((_)/ \<turnstile> (_))\<close> [6,6] 5)
-  "_Context"  :: "two_seqe"   (\<open>((_)/ :=: (_))\<close> [6,6] 5)
+  "_Trueprop" :: "single_seqe" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
+  "_Context"  :: "two_seqe"   (\<open>(\<open>notation=\<open>infix Context\<close>\<close>(_)/ :=: (_))\<close> [6,6] 5)
   "_PromAux"  :: "three_seqe" (\<open>promaux {_||_||_}\<close>)
 
 parse_translation \<open>