Hi. Can the toplevel interpret itself? I'd like to reduce boilerplate by introducing some macros, preparing sequences of toplevel commands as strings and interpreting them as if they had been written like that in the theory buffer. Is that possible?
So far, I always opened up the definition of the toplevel commands in question and replicated them in a piece of custom ML, but that is rather cumbersome.
Last updated: Dec 07 2023 at 12:30 UTC