Isabelle tactic for Lisa proofs

[vkuncak]

Using Eisbach tactic language of Isabelle ( https://trustworthy.systems/projects/TS/tactics )
develop a tactic to check kernel proofs in Isabelle/FOL printed using updated version of Isabelle printer.

[SimonGuilloud]

This would involve writing Isabelle automation for OCBSL, which may be interesting in itself.