File: transform_win.doc

package info (click to toggle)
hol88 2.02.19940316-28
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 65,924 kB
  • ctags: 21,595
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,075; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (28 lines) | stat: -rw-r--r-- 784 bytes parent folder | download | duplicates (11) 
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
 
\DOC transform_win

\TYPE {transform_win : (thm -> window -> window)}

\SYNOPSIS
Transform the focus of a window.

\LIBRARY window

\DESCRIBE
{transform_win (H |- f' R f)} transforms the focus of a window
from {f} to {f'}.

\FAILURE
{transform_win (H |- f' R f) w} will fail if {f} is not the focus
of the window {w}.
If {H} is not a subset of the context of the window {w},
then {transform_win (H |- f' R f) w} will fail.
{transform_win (H |- f' 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, match_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