On Fri, 29 Oct 2010, Tobias Nipkow wrote:
Unless I have a lapse of memory, the timeout specifications for s/h and
Nitpick are also in seconds, possibly with an "s" appended. As a user I
am glad about that, because I do not think in ms and would not like to
write 30000 instead of 30.
I have forgotten to say that Jasmin has his own (complicated) time
formats.
This is again a question how we invest our own precious time (by keeping
things as simple as possible) while minimizing user confusion.
Makarius
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
