src/HOL/Library/LaTeXsugar.thy
changeset 21964 df2e82888a66
parent 21210 c17fd2df4e9e
child 22328 cc403d881873