[isabelle] Sequents evaluation


I'm sorry for disturbing you with the question, which may be quite
silly. I want to use Isabelle for some very simple temporal reasoning by
modal logic. Neither S4, neither Modal0 nor other modal thys aren't
covered in logics.pdf. ☹
I starred on corresponding files and twisted them as I could, but didn't
found any natural way to evaluate propositions in Sequents logic. Is
there some hidden door, walkaround or a simple decision I missed?

Thanks in advance!
Сергей Каунов <skaunov at gmail.com>

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.