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
|
\DOC print_all_thm
\TYPE {print_all_thm : bool ref}
\SYNOPSIS
Flag determining whether the assumptions of theorems are printed explicitly.
\DESCRIBE
The reference variable {print_all_thm} is one of several
settable parameters controlling printing of terms by {pp_print_term}, and hence
the automatic printing of terms and theorems at the toplevel.
When it is {true}, as it is by default, all assumptions of theorems are
printed. When it is {false}, they are abbreviated by dots.
\FAILURE
Not applicable.
\EXAMPLE
{
# let th = ADD_ASSUM `1 + 1 = 2` (ASSUME `2 + 2 = 4`);;
val th : thm = 2 + 2 = 4, 1 + 1 = 2 |- 2 + 2 = 4
# print_all_thm := false;;
val it : unit = ()
# th;;
val it : thm = ... |- 2 + 2 = 4
}
\SEEALSO
pp_print_term, prebroken_binops, print_unambiguous_comprehensions,
reverse_interface_mapping, typify_universal_set, unspaced_binops.
\ENDDOC
|
