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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and