On Thu, May 31, 2012 at 1:36 PM, Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
