src/HOL/Library/LaTeXsugar.thy
changeset 21619 dea0914773f7
parent 21210 c17fd2df4e9e
child 22328 cc403d881873