UI-TAC : TACTICUI-TAC is a tactic.
As defined for use NAT-DED: is a primitive tactic.
If a support line is universally quantified, will instantiate it. In
interactive mode will ask for a term, otherwise will use the bound
As defined for use ETREE-NAT: is a primitive tactic.
If a support node is an expansion node with an admissible expansion,
applies universal instantiation. Pfenning's tactics 204/205. If a support
line has multiple expansions, it will be duplicated, with the duplication
receiving just the excess expansion terms. The instantiated line will
not become a support of any other goal than the current one, since it
is not known if it is yet admissible for others. The original support
line will be dropped from the supports of the current goal, but
remain as a support for any other goals. The new support lines
will be supports only for the current goal.
TPS documentation homepage