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