[isabelle-dev] Move `Eisbach`, `rewrite` etc. to Pure

Joshua Chen isabelle-dev at joshchen.io
Wed Mar 25 10:38:33 CET 2020

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.


More information about the isabelle-dev mailing list