[isabelle-dev] quickcheck on type real

Tobias Nipkow nipkow at in.tum.de
Sun Sep 2 07:49:10 CEST 2007


> *** DIVZERO
> *** At command "quickcheck".

I also ran into this one (and notified Stefan).

> lemma "inverse (a::real) = (1 / a)"
> 
> Counterexample found:
> a = -1

I love it, a false counterexample to a false thm ;-)

Thanks!
Tobias



More information about the isabelle-dev mailing list