[isabelle] Word authorship

Hi all,

I want to take attention to a maintainance issue concerning the
different word-related session.  IMHO these are:

1) HOL-Word (in the distribution)
	Authors: a couple (according to theory file headers)

2) Word_Lib (in the AFP)
	Authors: many (according to official AFP meta data)

3) Native_Word (in the AFP)
	Authors: one plus one contributor (according to official AFP
          meta data)

1) and 2) are collections around word types, whereas 3) has a particular
focus, an observation which is based both on content and the number of

2) and 3) have a tendency to augment developments from HOL-Word or other
HOL sessions in order to serve a certain purpose better.  An example:
Native_Word provides code equations for symbolic computation of bit
operations on ints, something which is typically directly provided by
the corresponding session.

In the past this has already led to a silent spreading of material from
2) and 3) to 1), without a particular attribution of authorship.

On the one hand, it is not so uncommon that scattered generic material
from AFP entries (often organized in theories named More_*, Auxiliary,
Preliminaries, …) finds its way to the distribution.

On the other hand, this time the restructuring might turn out more
extensive in the end and deserve more explicit attribution of
authorship: one idea is that eventually HOL-Word vanishes into two or
three library theories in the distribution and special operations end up
in Word_Lib (caveat: this is just an idea).

What do the authors of these sessions think?


Attachment: signature.asc
Description: OpenPGP digital signature

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