Manip user’s guide, version 1.3. Sequent manipulations for an interactive prover such as PVS can be labor intensive. We provide an approach to tactic-based proving for improved interactive deduction in specialized domains. This approach has been mechanized by the Manip package of strategies (tactics) and support functions. Although it was designed originally to reduce the tedium of low-level arithmetic manipulation, many of its newer features are suitable as general-purpose prover utilities. Besides strategies aimed at algebraic simpli cation of real-valued expressions, Manip includes term-access techniques applicable in arbitrary settings.