[isabelle-dev] Nominal and FinFuns from the AFP
huffman at in.tum.de
Thu May 31 15:56:03 CEST 2012
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
>>> 'include' syntax in local situations.
>> I tried to implement the new syntax for FinFuns with bundles and Brian's
>> notation attribute
>> 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.
If you want to call one of my ideas a "bad idea", then I hope you have
a better justification for this statement.
More information about the isabelle-dev