[isabelle-dev] MIR decision procedure

Lawrence Paulson lp15 at cam.ac.uk
Fri Nov 13 17:05:16 CET 2015

The MIR decision procedure is again working. We still have the mystery of what it is good for. It is not used anywhere at all. Even the test suite consists of a mere five problems. And I have now stumbled across ferrack. It seems to be used quite a bit, but what does it do? Is it documented anywhere?


More information about the isabelle-dev mailing list