Am 02.11.2010 um 14:08 schrieb Makarius: > The scheme of seconds as float addresses the intuition of at least 3 others > on this thread, as well as Jasmin's requirement to re-scale numbers. > > It only makes sense to make this move, if we arrive at a single standard in > the end, instead of four of them.
Floating-point numbers are a decent alternatives, and seconds, being the standard unit for time in physics and elsewhere, makes sense; hence, I will not stand in the way of standardization. (My personal preference does remain for a unit suffix, e.g., "s", for readability's sake, though.) A very minor issue is that I was never able to parse options like nitpick [timeout = 1.5] even with custom parsers, unless 1.5 is doubly-quoted. Users might not realize they need quoting and will most probably be confused by the resulting error. Jasmin _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev