(*<*) section ‹Hyper CTL*› theory HyperCTL imports Finite_Noninterference begin (*>*) (*<*) end (*>*)