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.


	Makarius





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