# Isabelle/HOL sequents: meaning of types o, seq', meaning of nonterminals seq, seqobj, seqcont

I am trying to understand https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/Sequents.html and https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/Sequents/Sequents/ILL.html and I have problems with the understanding the meaning of the basic items, namely:

types o, seq'

nonterminals seq, seqobj, seqcont?

Do these types and nonterminals have some "real world" counterparts? Sequent is represented by function [o, seq']=>seq', so, maybe o and seq' do not have any real world counterparts?

I am reading "Isabelle's Logics" (http://isabelle.in.tum.de/dist/Isabelle2016-1/doc/logics.pdf especially chapter 4), LNCS 828, Isabelle/Isar reference manual (especially 8.2 and 8.5 about mixfix notations and syntax definition), but I can not grasp the meaning of those symbols and therefor I can not move forward. Any guidance would be very helpful!

I am trying to implement monoidal logic http://www.sciencedirect.com/science/article/pii/S1570868314000573 as a object logic in Isabelle/HOL, but everything is so detached from the "real world" (how the mathematics is being done on paper).

• Such theorem-provers have a VERY steep learning curve indeed. Perhaps I am just not clever enough, but I gave up and had to write my own proof assistant. It was great fun! You can download it at dcproof.com but it may not help much with monoidal logic. If you don't like the axioms I have built in, you can play around and introduce your own. – Dan Christensen Aug 22 '17 at 21:09