Abella 1.3.3

6 views
Skip to first unread message

Andrew Gacek

unread,
Jan 21, 2010, 9:48:01 AM1/21/10
to abella-the...@googlegroups.com, Todd Wilson
I'm pleased to announce the release of Abella 1.3.3. The new version
is available at http://abella.cs.umn.edu/ and a detailed list of
changes follows:

* Optimized the handling of state information. Based on the
developments included in the distribution, Version 1.3.3 is 150%
faster than Version 1.3.2.

* Added evaluation by explicit substitution development
contributed by J. Todd Wilson.

* Added Show command to display previously proved theorems.

* Added Split command to easily separate mutually inductive theorems.

* Fixed an issue with subgoal numbering.

* The apply tactic no longer requires "dummy nominals" when nabla
bound variables in a lemma are not used.

* The search tactic now backtracks over equalities.

* The search tactic now properly considers all nominal constants
when trying to instantiate an existential.

* The cut tactic can now be used without a 'with' argument in
which case the search tactic is used to find possible hypotheses to
cut from a specification judgment.

-Andrew

Reply all
Reply to author
Forward
0 new messages