[isabelle] Commandline results for quickcheck / nitpick



Hi everyone,

quickcheck and nitpick provide great feedback within the jedit IDE. Using "isabelle build" to build a theory containing one of these commands doesn't work, however. It's possible that I'm doing something wrong, but it seems like a theory is invalid if it contains one of these commands. Is this true - are they only for interaction purposes, not to count as results of the theory? 

This would make sense, since the goal is a checked proof after all. Still, it is convenient to see these counterexamples sometimes, and seeing them from the command line would be nice.

Does anyone have any useful information regarding this? Thanks.




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