[isabelle] Redefine or hook into the outer-syntax keywords
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
keywords "theorem", "lemma" etc.
This archive was generated by a fusion of
Pipermail (Mailman edition) and