The pvs-strategies file for airline.dmp

(defstep lazy-grind  (&optional (if-match t) (defs !) rewrites
                                theories exclude (updates? t))
   (then
     (grind$ :if-match nil :defs defs :rewrites rewrites 
             :theories theories :exclude exclude :updates? updates?)
     (reduce$ :if-match if-match :updates? updates?))
  "Equiv. to (grind) with the instantiations postponed until after simplification."
  "By skolemization, if-lifting, simplification and instantiation")

(defstep stew (&optional lazy-match (if-match t) (defs !) rewrites theories
               exclude (updates? t) &rest lemmas)
   (then
     (if lemmas 
       (let ((lemmata (if (listp lemmas) lemmas (list lemmas)))
	     (x `(then ,@(loop for lemma in lemmata append `((skosimp*)(use ,lemma))))))
          x)
       (skip))
     (if lazy-match 
       (then (grind$ :if-match nil :defs defs :rewrites rewrites
                     :theories theories :exclude exclude :updates? updates?) 
             (reduce$ :if-match if-match :updates? updates?))
       (grind$ :if-match if-match :defs defs :rewrites rewrites
                     :theories theories :exclude exclude :updates? updates?)))
"Does a combination of (lemma) and (grind)."
  "~%Grinding away with the supplied lemmas,")