src/HOL/Library/LaTeXsugar.thy
changeset 55915 607948c90bf0
parent 55114 0ee5c17f2207
child 55954 a29aefc88c8d