Added unfolding/folding functions in defs module.
Fix interactive mode compilation bug.  Add parsing function for
formulas.  Unfolding rules now use the appropriate Sl_defs functions.
Added commented-out code for printing trace pair info in proofs.  Some
code reviewed in the SL and while rules.