[isabelle] Printing instantiations



Hi all,

I was wondering whether it's possible to print out the instantiations
returned by Thm.first_order_match. Since it returns the type (ctyp * ctyp)
list * (cterm * cterm) list, is there a way to convert this type to a
string? I just want to test it to see what the instantiations look like.
Should I actually bother?

Thanks
Steve




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