header {*\isaheader{Refinement Framework}*} theory Refine_Monadic imports Refine_Chapter Refine_Basic Refine_Heuristics Refine_While Refine_Foreach Refine_Transfer Refine_Pfun Refine_Automation Autoref_Monadic begin text {* This theory summarizes all default theories of the refinement framework. *} end