* 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