[isabelle-dev] Word Libraries

[Florian Haftmann]

Hi Gerwin et. al.,

>> C. Poor man's genericity 32 vs. 64
>>
>>> What is the state supposed to be achieved here?  Naively I would think
>>> that Word_Setup_ARCH.thy should contain all »generic« lemmas and make
>>> use of the »generic« type alias, whereas »specific« lemmas should stay in
>>> Word_32 / Word_64.
> 
> Yes, that would make sense and would clarify the setup. It is possible that some lemmas are not in the right place due to dependencies, but a lot of material has been generalised and moved into generic Word_Lemmas instead, so it is quite possible that this could now be applied consistently.

I have arranged this now in

isabelle: d1117655110c
afp: 0b1dccde39f0

This his been my tentative last work on that before the upcoming release.

Are there still issues I should look after?

Cheers,
	Florian



-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211104/4cc6b37c/attachment.sig>