src/HOL/Library/LaTeXsugar.thy
changeset 63149 f5dbab18c404
parent 63120 629a4c5e953e
child 63414 beb987127d0f