[isabelle-dev] Word Libraries
florian.haftmann at informatik.tu-muenchen.de
Thu Nov 4 12:11:31 CET 2021
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
This his been my tentative last work on that before the upcoming release.
Are there still issues I should look after?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev