[isabelle-dev] NEWS / CONTRIBUTORS

[Lukas Bulwahn]

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