--- a/src/Sequents/ILL.thy Sun Sep 22 16:04:44 2024 +0200
+++ b/src/Sequents/ILL.thy Sun Sep 22 16:12:15 2024 +0200
@@ -29,7 +29,7 @@
PromAux :: "three_seqi"
syntax
- "_Trueprop" :: "single_seqe" (\<open>(\<open>notation=\<open>infix Trueprop\<close>\<close>(_)/ \<turnstile> (_))\<close> [6,6] 5)
+ "_Trueprop" :: "single_seqe" (\<open>(\<open>notation=judgment\<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>)