Holbert 0.5 is now live on http://liamoc.net/holbert.
It now supports inductive judgements, induction and rule inversion, better unification solutions, many bug fixes, better rewriting support, and many other small improvements. This is mostly due to the great work from my two undergrads over the last year, Chris Perceval-Maxwell and Rayhana Amjad.
If you see an error message on load, you may have to clear your cache.
Lecturer at LFCS, University of Edinburgh. I leave these toots, I do not know for whom. I no longer know what they are about.
Formal Methods, Verification, Concurrency, etc.