[isabelle-dev] time specifications

[Makarius]

On Tue, 2 Nov 2010, Makarius wrote:

> We can now move forward to standardize time specifications as follows:
>
>  * Time is in seconds, as double precision floating point; users can
>    write 1 or 1.0 or 1.5 etc.
>
>  * A one-line function ML seconds: real -> Time.time deflates the
>    many variations of Time.fromFoo (typical bulky NJ library design).
>
>  * ISABELLE_HOME_USER acquires an extra prefix for *named* distributions,
>    i.e. official releases or bightly builds (not compilations from the
>    repository) to allow changing the meaning of former
>    settings in milliseconds.  (This helps robustness of installations in
>    general, not just for timeouts.)

There are still some fine points missing, but those using seconds as 
integers can easily upgrade to floats now, using the ML function called 
"seconds" together with Attrib.config_real or Parse.real.

Also note that string_of_real helps to print reals in a simple way 
(without having to specify custom formats).


 	Makarius