Enable Quickcheck in Isabelle check file

[wimmers]

We can write something like this in the check file:
lemma
"Submission.x = x"
quickcheck [expect = no_counterexample]
sorry

Then the submission will be rejected if quickcheck finds a counterexample.

If we just want to deduct something from the score for this kind of error, I do not see a way to do it currently, however.
For that one would have to wrap up quickcheck in a fake tactic that fails if a counterexample is found
or else “proves” the goal with an oracle that is not sorry (“a good sorry”).