Hi Florian,
Thanks for all this.
2. Meanwhile, I really like the new simplifier tracing facility and
hardly ever use the old [[simp_trace]]. Since the new trace offers a lot
of control over the tracing, would it make sense to base the tracing
facility on the new one?
It would definitely make
*** System ***
* The Isabelle tool update_cartouches changes theory files to use
cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
This refers to Isabelle/fffdbce036db. In the subsequent changesets, I
have modernized a few of my own hotspots accordingly, but refrained
