src/HOL/Library/LaTeXsugar.thy
changeset 56519 c1048f5bbb45
parent 56245 84fc7dfa3cd4
child 56977 a33fe940a557