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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
