CongrM widget #
This file defines a congrm?
tactic that displays a widget panel allowing to generate
a congrm
call with holes specified by selecting subexpressions in the goal.
CongrM widget #
Return the link text and inserted text above and below of the congrm widget.
Equations
Instances For
Rpc function for the congrm widget.
Equations
Instances For
The congrm widget.
Equations
Instances For
Display a widget panel allowing to generate a congrm
call with holes specified by selecting
subexpressions in the goal.