src/HOL/Library/LaTeXsugar.thy
changeset 58187 d2ddd401d74d
parent 56977 a33fe940a557
child 60500 903bb1495239
equal deleted inserted replaced
58186:a6c3962ea907 58187:d2ddd401d74d