[isabelle] Using counter example finder and 'a-types




I'd like to use Isabelle's counter-example finder, but unfortunately often on conjectures with polymorphic types (eg. 'a list), which is not supported as far as I know. Does anyone have any tips or hacks to work around this, such as pretending the 'a list is a list of integers or something like that?

Cheers,
Moa Johansson





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