Re: [isabelle-dev] NEWS / CONTRIBUTORS
On 09/12/2011 07:29 PM, Florian Haftmann wrote: Hi Lukas, the rename AssocList ~ AList_Impl should sound AssocList ~ AList Nota bene: T.thy – theory as intended to be used by other theoreis T_Impl.thy – implementation for abstract type Since ALists are not abstract, there is no AList_Impl.thy, but cf. RBT_Impl.thy. The rename AssocList ~ AList will be fruitful in the middle run: generic operations with popular names should be qualified, and AssocList.update will not do. The data structure library theories then can orient more and more towards the Isabelle/ML library (fragments of this intension already showing up in More_List.thy). Florian The rename AssocList to AList_Impl was actually already glimpsing into the future, where there will exist an abstract AList, as our brave users have already done this in the AFP-Collections framework. I now followed your suggestion, but in the future, this will be revised once again, until the Isabelle/ML library and the HOL/Library theories coincide. Lukas ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS / CONTRIBUTORS
Hi Lukas, the rename AssocList ~ AList_Impl should sound AssocList ~ AList Nota bene: T.thy – theory as intended to be used by other theoreis T_Impl.thy – implementation for abstract type Since ALists are not abstract, there is no AList_Impl.thy, but cf. RBT_Impl.thy. The rename AssocList ~ AList will be fruitful in the middle run: generic operations with popular names should be qualified, and AssocList.update will not do. The data structure library theories then can orient more and more towards the Isabelle/ML library (fragments of this intension already showing up in More_List.thy). 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 signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS / CONTRIBUTORS
My impression is that NEWS and CONTRIBUTORS for the coming release is still somewhat incomplete. NEWS is not just for bad news -- infamous INCOMPATIBILITY entries -- but for any user-relevant changes. If things are not user-relevant then what is the point of doing them in the first place? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
