SASyLF version 0.20 - partial support for mutual induction

[Jonathan Aldrich]

SASyLF version 0.20 is now available at
http://www.cs.cmu.edu/~aldrich/SASyLF/SASyLF-0_20.zip

I've added syntactic support for mutual induction to SASyLF in a very
simple way:

theorem Thm1: ...
...
d2: XXX by theorem Thm2 on d1
...
end theorem
and
theorem Thm2: ...
...
d4: YYY by theorem Thm1 on d3
...
end theorem

We don't yet check that the mutual induction is well-founded (i.e.
recursive calls are to subderivations) so SASyLF produces a "not checked
yet" warning when there is a forward reference to a theorem. The
attached file shows a simple example of the syntax (although the theorem
isn't really recursive, I just put things in the wrong order to show it
is possible).

Changelog:
* Fixed bug in input freeness checking, and redid the way case
analysis works
* Checked for using a non-variable where a variable is expected in a
judgment
* Implemented "and theorem" syntax to allow mutual induction (but we
don't yet check that mutual induction is well-founded)

Jonathan