[POPLmark] Poplmark Digest, Vol 10, Issue 5

[Michael Norrish]

I have put a HOL4 solution onto the web at

  http://users.rsise.anu.edu.au/~michaeln/poplmark/wangScript.sml

It uses my existing type of lambda-calculus terms.  These support
capture-avoiding substitution, free-variables etc. 

I've commented the script a little.  Adam's proof (just posted) is
about possibly capturing substitution, so he doesn't need to worry
about renaming variables etc.  I can get around this by deriving a BVC
rule induction principle, but without Isabelle's automatic support for
doing this, the length necessarily increases.

Michael.