[isabelle-dev] NEWS

[Makarius]

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