-
SimonGuilloud authored
* OL solver * Optimizations for Tautology solver, dedicated proof tactic, comments and scaladoc. * When failing to prove a sequent, Tautology now reports on what is the missing piece that prevented from concluding the proof in the error message. * Good reorganisation of lisa.utils, comments. * correct issue preventing test runs failing on some proof in a test library to go through correctly. * dsl to get definitions of symbols as justification
SimonGuilloud authored* OL solver * Optimizations for Tautology solver, dedicated proof tactic, comments and scaladoc. * When failing to prove a sequent, Tautology now reports on what is the missing piece that prevented from concluding the proof in the error message. * Good reorganisation of lisa.utils, comments. * correct issue preventing test runs failing on some proof in a test library to go through correctly. * dsl to get definitions of symbols as justification