[isabelle] Redefine or hook into the outer-syntax keywords



Dear all,

Is it possible to redefine the outer-syntax keyword "theorem"
or hook into it?

I am in the process of defining a new object logic. There,
I would like the keyword "theorem" to analyze the user-given
statement, and add assumptions to it.

I have so far been working with a different outer-syntax keyword
("mytheorem"), but I wonder if it would also be possible to use the
existing
keywords "theorem", "lemma" etc.

Regards,

Cezary




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