[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]