Re: [isabelle] Custom inner syntax parsing in ML.



I would like to congratulate Christian on his sense of humour!

Tobias

On 02/10/2019 10:51, Urban, Christian via Cl-isabelle-users wrote:

The otherwise very great tutorial at https://
nms.kcl.ac.uk/christian.urban/Cookbook/ is unfortunately still lacking
information on parse translations and generally on intervening on the inner
syntax parsing process - in fact I'm considering to contribute to it once my
own project is done.

That document is "fan-fiction". In its early years, I tried to
contribute to it and rectify its somewhat misleading approach at
"Isabelle system hacking", but I've given up on it long ago.

Thanks for the praise from everybody....I would have interpreted "darkfic"
as criticism. ;o)

Anyway, if anybody likes to contribute "fix-fic" [*], you download the sources, make
changes and send back the diffs. Norbert Schirmer did this recently by getting
the fan-fiction back into a compilable state with Isabelle 2019. All praise to him!

Best wishes,
Christian


[*] https://en.m.wikipedia.org/wiki/Fan_fiction


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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