Prolog -- A bare-bones implementation of Lambda-Prolog

This is a simple exploratory implementation of Lambda-Prolog in HOL, including some minimal examples (in Test.thy) and a more typical example of a little functional language and its type system.