* The split tactic now operates on n-ary conjunctions
* Tactic names no longer conflict with terms during parsing
* Added the monotone tactic which explicitly realizes the
monotonicity property of specification logic contexts
* Fixed a couple unification bugs
* New examples
o path - equivalence of lambda terms based on the paths through terms
o cut - this cut admissibility example has been updated to
include all operators of the sequent calculus
o pi - specification of late pi-calculus and strong bisimulation
-Andrew