src/HOL/Library/LaTeXsugar.thy
changeset 55370 e6be866b5f5b
parent 55114 0ee5c17f2207
child 55954 a29aefc88c8d