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