[isabelle-dev] NEWS

Alexander Krauss krauss at in.tum.de
Tue Feb 1 21:15:58 CET 2011

* 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.


More information about the isabelle-dev mailing list