[initial checkin of new verifier
raph.levien@gmail.com**20090620053022] 
[gently hacking on javascript implementation
raph.levien@gmail.com**20090626055224] 
[strip parens from proof; check disjoint binding vars
raph.levien@gmail.com**20090627060428] 
[free variables now checked
raph.levien@gmail.com**20090729212732] 
[a little more in the javascript port
raph.levien@gmail.com**20091012051911] 
[adapting mm_xlat for new ghilbert changes
raph.levien@gmail.com**20091013225317] 
[support for compressed proofs in mm_xlat
raph.levien@gmail.com**20091014055005] 
[fix problem in mm_xlat, set.mm almost verifies
raph.levien@gmail.com**20091017223304] 
[get peano_thms to pass in new verifier
raph.levien@gmail.com**20091018042338] 
[prove distributive law of peano arithmetic
raph.levien@gmail.com**20091023231852] 
[up to mulcom in peano; more js code (not tested yet)
raph.levien@gmail.com**20091026042630] 
[fixes to js; it now successfully verifies peano_thms
raph.levien@gmail.com**20091101035048] 
[a start at editing with cut'n'paste
raph.levien@gmail.com**20091107224632] 
[editor features: undo, up/down arrows, im translation
raph.levien@gmail.com**20091108081042] 
[first cut at interactive verification
raph.levien@gmail.com**20091111073003] 
