* be added to the output of pp_term.
* set to false if you need, for example, cut and paste from matitac output to
* matitatop *)
* be added to the output of pp_term.
* set to false if you need, for example, cut and paste from matitac output to
* matitatop *)