STD: defsum now generates some basic theorems

VL: some progress toward SystemVerilog expressions
 - Switched vl-atomguts-p to use defsum
 - Minor fixes to the lexer to support '$'
 - New atomic expression types for 'null', 'this', '$', time literals,
   and unbased unsized integers.
 - Parsing and pretty-printing support for these new expressions
 - Added unit tests about parsing these new expressions

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2539 303c5b2c-9740-0410-b014-fd8f9db7be32
very minor tweak to make_cert_help.pl set-max-mem reporting

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2540 303c5b2c-9740-0410-b014-fd8f9db7be32
tweak quicklisp install to load the 2014-01-13 distribution, partly to avoid potentially problematic iolib updates on 2014-02-12

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2541 303c5b2c-9740-0410-b014-fd8f9db7be32