(*<*) theory ICF_Entrypoints_Chapter imports Main begin (*>*) text_raw ‹\isasection{Entry Points}› (*<*) end (*>*)