Isabelle tactic for Lisa proofs
Opened this issue · 1 comments
vkuncak commented
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 commented
This would involve writing Isabelle automation for OCBSL, which may be interesting in itself.