* New term style "isub" as ad-hoc conversion of variables x1, y23 into
subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
For use in document preparation, e.g.,
lemma foo: "P x1 x2" <proof>
text {*
@{thm (isub) foo}
*}
produces output with subscripts. Converts names of Frees, Vars and Bounds.
Alex