[isabelle] Accessing split-theorems on ML-level



Hi,
I need to get hold of theorems for splitting case-statements, given a datatype, on the ML level (eg. theorems like "list.split", "nat.split" etc). Where can I find these?

Thanks,
Moa





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