updates to SymEval.

- This is enough to actually apply the seq_rule
- The current implementation of the assign rule is not
  correct. That comes next.
symbolic evaluation seems to work for simple cases.
working on getting Read to work

- this shows what kind of proofs that I need to do.
an update to symbolic evaluation and the imp language.
integrated the canceller into symeval2

- bug fixes in SepLogFold
  - now tests for purity and emp in all cases
- make the canceller visible
- lots of integration in SymEval2
a cleaned up version of symbolic evaluation

- Added skip, factored out the syntax
Next goal: swap
some progress on simplification.
purity is not simple.
Beginning to end proof of swap, but it isn't correct.

- The cancellation algorithm does not add any pure
  facts to the framing procedure.
Adding frame support to the canceller

- BUG: There is a problem with re-introducing
  existential quantification.
beginning to end symbolic evaluation of swap.
fix to STacCancel.
migrating to the newer STac.
Added a Java folder and briefly started work on the tactics for symbolic
execution of Java.

Added i MirrorCharge root folder for name spacing reasons.
Added axiomatic support for a list membership tactic.
Added tactics for list membership and NoDup.
intermediate updates.
Merge branch 'lambda' of github.com:jesper-bengtson/MirrorCharge into lambda

Conflicts:
	MirrorCharge!/CoqoonMakefile
Started adding support for Java tactics.