Extrategies is a set of strategy combinators and Lisp functions for writting strategies in PVS. Extrategies also contains improved versions of standard PVS strategies for skolemizing, naming, labeling, replacing, splitting, etc.

Extrategies has been part of PVS since PVS 5.0. The current version of Extrategies
is 6.0 and is included in PVS 6.0. Extrategies 6.0 is a significant revision of
the previous version. Extrategies 6.0 handles TCCs in a much cleaner
way and includes several new strategy combinators for writting strategies. It also
includes the proof command `deftactic`

for defining local strategies
(called tactics), whose scope is the branch of the proof where the
tactic is declared.

The strategies included in Extrategies 6.0 are:

- Printing and commenting:
`printf`

,`commentf`

- Defining tactics, i.e., local strategies:
`deftactic`

- Labeling and naming:
`unlabel*`

,`delabel`

,`relabel`

,`name-label`

,`name-label*`

,`name-replace*`

, discriminate - Copying formulas:
`copy*`

,`protect`

- Programming:
`mapstep`

,`mapstep@`

,`with-fnums`

,`with-fnums@`

- Control flow:
`finalize`

,`touch`

,`for`

,`for@`

,`when`

,`when@`

,`unless`

,`unless@`

,`when-label`

,`unless-label`

,`if-label`

- Skolemizing, let-in definitions, instantiating:
`skeep`

,`skeep*`

,`skoletin`

,`skoletin*`

,`redlet`

,`redlet*`

,`skodef`

,`skodef*`

,`insteep`

- TCCs:
`tccs-expr`

,`tccs-formula`

,`tccs-formula*`

,`tccs-step`

,`with-tccs`

- Miscellaneous:
`splash`

,`replaces`

,`rewrites`

,`rewrite*`

,`suffices`

This list is printed by the proof command
- Examples
- Real Automation in the Field, César Muñoz and Micaela Mayero, Contractor Report ICASE, NASA/CR-2001-211271, 2001. BibTex Reference

`extrategies-about`

.
The behavior of some strategies in Extrategies
6.0 may be slightly different from previous
versions. Because of this, some proofs that worked in PVS 5.0 may be broken in
PVS 6.0. In particular, `skoletin`

may generate formulas in a different order. In most cases, the old
behavior of `skoletin`

can be simulated by setting the
option `:old?`

to `t`

.