Document mysterious useful comments for ctac and ceqv

[Xaphiosis]

There is this comment, in CSpace_C:

(* Useful:
  apply (tactic {* let val _ = reset CtacImpl.trace_ceqv; val _ = reset CtacImpl.trace_ctac in all_tac end; *})
  *)

This should be moved to CTac.thy, but also documented in crefine-notes.md, after first investigating what exactly it does.

The same goes for (same file):

(* ML "set CtacImpl.trace_ctac"*)