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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
\DOC assignable_print_term
\TYPE {assignable_print_term : (term -> void)}
\SYNOPSIS
Assignable term-printing function used for printing goals.
\DESCRIBE
The printing of terms can be modified using the ML directive {top_print}.
However the term printing functions used for printing goals are not affected
by {top_print}. To make use of user-defined print functions in goals, the
assignable variable {assignable_print_term} must be changed.
\EXAMPLE
{
#let my_print_term tm =
# do (print_string `<<`;print_term tm;print_string `>>`);;
my_print_term = - : (term -> void)
#"x ==> y";;
"x ==> y" : term
#top_print my_print_term;;
- : (term -> void)
#"x ==> y";;
<<"x ==> y">> : term
}
{
#g "(x ==> y) /\ (y ==> x) ==> (x = y)";;
"(x ==> y) /\ (y ==> x) ==> (x = y)"
() : void
#expand (REPEAT STRIP_TAC);;
OK..
"x = y"
[ "x ==> y" ]
[ "y ==> x" ]
() : void
}
{
#assignable_print_term := my_print_term;;
- : (term -> void)
#expand ALL_TAC;;
OK..
<<"x = y">>
[ <<"x ==> y">> ]
[ <<"y ==> x">> ]
() : void
}
{
#assignable_print_term := print_term;;
- : (term -> void)
#expand ALL_TAC;;
OK..
"x = y"
[ "x ==> y" ]
[ "y ==> x" ]
() : void
}
\SEEALSO
print_term, top_print.
\ENDDOC
|
