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
OpenPGP_signature
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
