1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
\DOC match_transform_win
\TYPE {match_transform_win : (thm -> window -> window)}
\SYNOPSIS
Transform the focus of a window.
\LIBRARY window
\DESCRIBE
{match_transform_win (H |- !x1...xn. g R f)} specialises the quantified
variables {x1} ... {xn} and then instantiates the free variables so that
{f} matches the focus of window. The focus is then transformed to
{g} (with the same substitutions applied).
\FAILURE
{transform_win (H |- g R f)} will fail if {f} can not be instantiated
to the focus of the window.
{transform_win (H |- g R f)} will fail if {H} is not a subset of the
context of the window.
{transform_win (H |- g R f)} will fail if {R} is not equal to or
stronger than the relation that the window is supposed to maintain.
\SEEALSO
transform_win, TRANSFORM_WIN, MATCH_TRANSFORM_WIN,
convert_win, CONVERT_WIN, rule_win, RULE_WIN,
thm_rule_win, THM_RULE_WIN, foc_rule_win, FOC_RULE_WIN,
tactic_win, TACTIC_WIN, rewrite_win, REWRITE_WIN
\ENDDOC
|
