This is probably the ultimate version of a long series of theorem provers and the simplest and most elegant version. The whole proof process is condensed and the system is much easier to use and test.
You can find the documentation
on the system on the Shen site including instructions for download. The system is configured to run under Shen-Scheme for Windows which is in downloaded as an executable. Clicking on the batch file will load stlib and THORN. But any S-version Shen with stlib installed will run THORN.