As I said, I was entirely unconfused that it is in seconds, and am glad of it. HOWEVER: there is indeed a confusing difference between s/h and Nitpick on the one hand and q/c on the other hand:
quickcheck[timeout=30] sledgehammer[timeout=30s] And also in their response to the wrong format: quickcheck[timeout=30s] *** Outer syntax error: end of input expected, *** but keyword [ was found sledgehammer[timeout=30] *** Parameter "timeout" must be assigned a positive time value (e.g., "60 s", "200 ms") or "none". *** At command "sledgehammer" Unification is appreciated ;-) Tobias Makarius schrieb: > 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