Re: [isabelle] New AFP theory: List Index



> But we wouldn't have to switch
> over everything at once---we could flesh out the hierarchy gradually,
> with input from the user community, and move libraries to their new
> places in the namespace one at a time.

A related issue: we have to encourage ourselves to factor out generic
formalisations from applications, as Tobias pointed out.  From my
perspective the four major obstacles are:

* little reputation in the strictly scientific sense;
* no real user interface support for refactoring activities;
* difficult to tinker with the bootstrap theories above Main.thy, even
for developers (a typical candidate would be List.thy);
* incoherence and duplication in existing theories themselves, which
make it difficult to decide what "the" way for contributed things
actually is.

But this leaves still room for contributions to HOL/Library or separate
AFP articles.  It would be interesting to hear experiences and comments
from users who have tried to factor out library theories from their
applications -- successes and failures.


Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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