Re: [isabelle] Multiset ordering vs. subset syntax



On Wed, 1 Apr 2015, Jasmin Blanchette wrote:

I am not sure whether it would be best to do the swap in one step.

Well, I am sure that I donât want 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.

I donât know how your fancy Perl scripts will deal with < and â, based on the type.

Perl is indeed mostly out -- Isabelle/Scala has token over regex operations quite successfully in recent years, together with convenient I/O operations that follow Isabelle/ML customs.

The problem to operate on sources systematically, based on actual formal content is rather old and well-known, but not yet done routinely. In principle, the PIDE markup could be used to guide the text replacement -- some genuine "refactoring" of theories.

I am not proposing this concretely right now, but the technology is pretty close to that.


	Makarius


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