% For HTML time: THEORY BEGIN time: TYPE = nat END time