This is a web-interface to Holfoot. Notice however, that in contrast to the full version running inside HOL 4, this web-interface has very restricted support for interaction. Please contact Thomas Tuerk if you have problems / suggestions / questions or simply want to learn more about Holfoot. For comparison, one can run Smallfoot as well. Example specifications ending in .sf should work with both tools. .dsf files contain Holfoot specific extensions and therefore produce parsing errors in Smallfoot. While .dsf files are intended to be close to the corresponding Smallfoot examples, .dsf2 files try to do it nicely in Holfoot. .hol files contain proof-scripts for complicated examples that need interaction.