[isabelle-dev] Nominal and FinFuns from the AFP

[Brian Huffman]

On Thu, May 31, 2012 at 1:36 PM, Makarius <makarius at sketis.net> wrote:
> On Thu, 31 May 2012, Andreas Lochbihler wrote:
>
>>> At some point, when I have bundles ready to work with the existing
>>> notation commands, we can fine-tune this scheme further, to allow users
>>> to
>>> 'include' syntax in local situations.
>>
>> I tried to implement the new syntax for FinFuns with bundles and Brian's
>> notation attribute
>> (https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2012-April/002585.html),
>> but it was not satisfactory.
>
>
> I did not have time yet to look more closely at that.
>
> Note that notation is based on "syntax declarations" of the local theory
> infrastructure, which is slightly different from what you have in
> attributes.  So notation as attributes is a bad idea.

Makarius:

If you want to call one of my ideas a "bad idea", then I hope you have
a better justification for this statement.

- Brian