added tbillc example to cli, added a parser for easier hol formula parsing (e.g. parse holformula "const P : i>o; const Q : i>i>o; var x,y:i; (all x (P(x) -> (exists y Q(x,y) )))" 

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1649 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
proper handling of +-*=, but some funny errors remain: (\ x => (\y => ( (x+x) = (y+y)  ))) does not parse, but (\ x => (\y => ( x+x = y+y  ))) does.

git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1650 85d21ef8-add0-11de-ae77-5bfb9c5a3f34
Fix m2e integration