Include/exclude sub-parts through options to \HOLthm etc

[mn200]

For \HOLthm and \HOLtm, it would be nice to “omit” certain sub-terms by specifying those terms in the optional arguments part of the command. Here “omit” means replace by “...” or similar. The interface could be to specify paths (as per PATH_CONV (1a41e14807)) to the terms to be omitted. Thus, something like

\HOLthm[o:bblr,o:bblllr]{thy.thmname}

would cause two sub-terms to be omitted. We might also extend the path language (for both this and PATH_CONV) to have things like c<digits> to allow easy specification of particular conjuncts.

Similarly, it might be nice to selectively include just a few constructors of a large datatype specification, perhaps via ic<digits> specifications (ic for include constructor), where something like

\HOLthm[ic1,ic3]{thy.datatype_tyname}

would give

tyname = C1 (args) | C3 (args) | ...

where the ... is effectively eliding constructors 2, 4, 5 etc.

Where multiple types are represented in the same recursion theorem, the constructor indexing could just be of the flattened list of all the types’ constructors.