prod and sum

* cleaner distinction between control symbols "\<^...>" and "\<^raw...>" in the scanner * output functions default_output and xsymbols_output only print one "\" for symbols (to be consistent with the scanner).

* Calculation commands "moreover" and "also" no longer interfere with current facts ("this"), admitting arbitrary combinations with "then" and derived forms.

'also'/'moreover': do not interfere with current facts, allow in chain mode;

export put_thms; do not export use_facts, reset_facts;

Added brief intro text.