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"*)
There is this comment, in
CSpace_C:This should be moved to
CTac.thy, but also documented increfine-notes.md, after first investigating what exactly it does.The same goes for (same file):