mechanical proof checkers for type soundness?

I'm looking for a good mechanical proof checker for type soundness 
proofs. I'm only interested in checking Wright-Felleisen-style 
soundness proofs over small-step operational semantics for Java-like 
languages, so I'd prefer it to be tailored as much as possible to that 
task. Any recommendations? Right now, I'm leaning toward Isabelle. 
Also, I'd prefer something that runs on Mac OS X, if possible.


Eric Allen
Sun Microsystems Laboratories