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 conceptually works.

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 map_data)?

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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.