Re: [isabelle] Proof_Context abstraction
On Tue, 29 Jul 2014, Joachim Breitner wrote:
and I started with the seemingly simple task of “For all local facts
with a name, add a "foo" to their name”.
That is not a simple task, and it does not quite fit to how Isabelle
The "implementation" manual provides a lot of background information, but
it needs to be studied carefully together with some canonical application.
Section "1.2 Names" might help a bit as a start in this particular case.
I’m trying to learn hacking Isabelle/ML
Is there a way to mess with the internals of the Proof_Context directly,
or would I have to change proof_context.ml for that (such as exposing
Or am I approach this task in a wrong way?
It depends whom you ask, and what you want to achieve. Proper
understanding the systems needs long time of study, not quick hacking. I
would go as far as to say that and "hacking" or "messing" is a not worth
the time spent on it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and