(* Title: Imperative_HOL_Time/Imperative_HOL_Time.thy Author: Maximilian P. L. Haslbeck & Bohua Zhan, TU Muenchen *) section ‹Entry point into monadic imperative HOL with time› theory Imperative_HOL_Time imports Array_Time Ref_Time begin end