(*<*) theory ICF_Chapter imports Main begin (*>*) text_raw‹\isachapter{The Original Isabelle Collection Framework}› text ‹ This chapter contains the original Isabelle Collection Framework. It contains a vast amount of verified collection data structures, that are included either directly or by parameterization via locales. Generic algorithms need to be instantiated manually, and nesting of collections (e.g.\ sets of sets) is not supported. › (*<*) end (*>*)