Re: [isabelle] Multiset ordering vs. subset syntax



Am Mittwoch, den 01.04.2015, 11:32 +0200 schrieb Florian Haftmann:
> Hi Jasmin,
> 
> > First step (for Isabelle2015):
> > 
> >    < and â for multiset inclusion
> >    #<# and #â# for the multiset ordering
> > 
> > The symbols â#<#â and â#â#â are ugly, but they would vanish with the expected Isabelle2016 release, at which point our proposal would be fully implemented. [*]
> 
> I am not sure whether it would be best to do the swap in one step.
> 
> In earlier days, we provided funny fix_foo tools (mostly perl scripts)
> which would assist in performing such transitions, and the multiset
> syntax IMHO looks feasible for this also.

Hm, maybe nowadays a Scala or ML script can do the job? How do you
otherwise distinguish btw. < for orders and < for multiset?


 - Johannes





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