[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Practicals: Programming with Tacticals

Announcement: Programming with Tacticals in PVS 
Practicals 2.1, a package for programming strategies in PVS with high
level tacticals, is available for PVS 3.1. Practicals enhances the PVS
proof language (IF, REPEAT, THEN, TRY, ...) with tacticals for looping
(WHILE, FOR), matching terms (MATCH), matching proof contexts (SCREEN),
raising proof failures (THROW), catching proof failures (CATCH), and
more ...

The package and the documentation are available at:

We welcome comments and user reports,

Florent Kirchner