author | wenzelm |
Thu, 06 Feb 2025 13:29:28 +0100 | |
changeset 82093 | a0b2cd020a8b |
parent 82092 | 93195437fdee |
child 82094 | 5b662ccae0af |
--- a/src/Pure/General/time.ML Thu Feb 06 12:46:13 2025 +0100 +++ b/src/Pure/General/time.ML Thu Feb 06 13:29:28 2025 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/General/time.scala Author: Makarius -Time based on nanoseconds (idealized). +Time based on nanoseconds (idealized), printed as milliseconds. *) signature TIME =