* 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
