Isabelle/HOL 序列：类型 o、seq' 的含义、非终端 seq、seqobj、seqcont 的含义

问：

我试图理解 https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html 和 https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html，但我在理解基本项目的含义方面有问题，即：

O型，以下'

非终端 seq， seqobj， seqcont？

这些类型和非终端是否有一些“现实世界”的对应物？Sequent 由函数 [o， seq']=>seq' 表示，所以，也许 o 和 seq' 在现实世界中没有任何对应物？

我正在阅读“Isabelle's Logics”（尤其是第 4 章）、LNCS 828、Isabelle/Isar 参考手册（尤其是关于 mixfix 符号和语法定义的 8.2 和 8.5），但我无法理解这些符号的含义，因此我无法继续前进。任何指导都会非常有帮助！

我试图在 Isabelle/HOL 中将单群逻辑 http://www.sciencedirect.com/science/article/pii/S1570868314000573 实现为对象逻辑，但一切都与“现实世界”（数学是如何在纸上完成的）脱节的。