(*<*) section ‹\isaheader{Examples for the Monadic Refinement Framework used with ICF}› theory Refine_Monadic_Examples imports Bfs_Impl Foreach_Refine Refine_Fold begin end (*>*)