src/HOL/Library/LaTeXsugar.thy
changeset 63325 1086d56cde86
parent 63120 629a4c5e953e
child 63414 beb987127d0f