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
|
\DOC remark
\TYPE {remark : string -> unit}
\SYNOPSIS
Output a string and newline if and only if {verbose} flag is set.
\DESCRIBE
If the {verbose} flag is set to {true}, then the call {remark s} prints the
string {s} and a following newline. If the {verbose} flag is set to {false},
this call does nothing. This function is used for informative output in several
automated rules such as {MESON}.
\FAILURE
Never fails.
\EXAMPLE
{
# remark "Proof is going OK so far";;
Proof is going OK so far
val it : unit = ()
# verbose := false;;
val it : unit = ()
# remark "Proof is going OK so far";;
val it : unit = ()
}
\SEEALSO
report, verbose.
\ENDDOC
|
