Added a simplified example of the semantics of the simply typed lambda calc in HOLCF. Cleaned up the proofs of type soundness and show both the isar and apply style versions