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



>> 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




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