src/HOL/Library/LaTeXsugar.thy
changeset 21404 eb85850d3eb7
parent 21210 c17fd2df4e9e
child 22328 cc403d881873