set_trace : string -> int -> unit
There is no single interpretation of what activity a tracing level should evoke: each tool registered for tracing can treat its trace level in its own way.
- set_trace "Rewrite" 1; - PURE_REWRITE_CONV [AND_CLAUSES] (Term `x /\ T /\ y`); <<HOL message: Rewrite: |- T /\ y = y.>> > val it = |- x /\ T /\ y = x /\ y : thm