Dear devs, Is there any plan to move Eisbach, the rewrite method and other non-HOL dependent tooling out from under the HOL library? Currently I have to make custom copies of e.g. rewrite when working in Isabelle/Pure because it imports Main. Best, Josh