(*<*) theory Collection_Autoref_Examples_Chapter imports Main begin (*>*) text_raw ‹\isasection{Automatic Refinement}› text ‹ This section contains examples of using the Collection Framework with the Automatic Refinement Framework. › (*<*) end (*>*)