Tactic: proc*

The proc* tactic applies to program-logic goals where the procedure(s) under consideration are referred to by name rather than content.

It replaces the procedure(s) with a statement calling that procedure. This is useful, for example, when the goal is relational, but one of the two procedures is abstract, while the other is concrete. In that case no variant of proc can be applied, but proc* can, after which things like inlining the concrete procedure can be used to make progress.

Syntax

proc*