Re: [isabelle] Make all selectors measure_functions?
On Fri, 12 Feb 2016, Richard Molitor via Cl-isabelle-users wrote:
I originally intended to get it into the AFP, but then never pushed it
when I got busy with applying for jobs and other things. The code is on
github though (https://github.com/gattschardo/open-inductive) and I made
it work with Isabelle2015 (and this week Isabelle2016-RC4).
I've already commented on an earlier version of this material, and you
seem to have improved it further. It generally looks good -- above the
average of various ML experiments that are already in AFP.
Some years ago, the AFP editors did not want to see actual ML tools there,
but de-facto we have that already.
Note that the "auto-magic" maintenance in AFP means that someone changing
certain Isabelle/ML things in Pure or HOL also goes through applications
in AFP and tries to adapt them. This sometimes requires to go over it with
the lawn-mower first, to put it into maintainable form. (Your sources look
quite maintainable already.)
I cannot say anything about the application, i.e. the problem that is
addressed here from a user perspective.
This archive was generated by a fusion of
Pipermail (Mailman edition) and