# [isabelle] Quickcheck counter example of "3 < 4"?

I forgot to add a type annotation and ended up with the following (Isabelle
2015 on Windows 7):
lemma "3 < 4" quickcheck
Quickchecking...
For instantiation with default_type Enum.finite_1:
Enum.finite_1 to be substituted for variable 'a does not have sort
{numeral,ord}
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
Compared with the type annotation:
lemma "(3::nat) < 4" quickcheck
Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found no counterexample.
Note: in the first case it says there is a counter example but that is the
end of the output in the "Output" tab of jEdit.
Is this to be expected when no types are given? As a new Isabelle user it
quite surprised me.
Thanks,
Jason

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*