This is a part of the Imperative HOL with Time development by Maximilian P. L. Haslbeck & Bohua Zhan, TU Muenchen

See https://github.com/bzhan/Imperative_HOL_Time

Included here with friendly permission by the authors.
