Document mysterious useful comments for ctac and ceqv

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"*)
```
