src/Sequents/S43.thy
changeset 80914 d97fdabd9e2b
parent 74302 6bc96f31cafd
--- a/src/Sequents/S43.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/Sequents/S43.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -14,7 +14,7 @@
              seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
 syntax
   "_S43pi" :: "[seq, seq, seq, seq, seq, seq] \<Rightarrow> prop"
-                         ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
+                         (\<open>S43pi((_);(_);(_);(_);(_);(_))\<close> [] 5)
 
 parse_translation \<open>
   let