[isabelle-dev] QuickCheck interface question

Moa Johansson moa.johansson at chalmers.se
Thu Oct 20 13:42:39 CEST 2011

I'm currently updating IsaPlanner and IsaCoSy to Isabelle2011-1. I noticed there are some changes to the QuickCheck interface:

The function test_term now takes an extra first argument of type compile_generator. What is this thing an how do I create one? Or even better, is there a default one? I noticed that test_terms (in plural) curiously does not take this extra argument.


More information about the isabelle-dev mailing list