src/HOL/Library/LaTeXsugar.thy
changeset 55982 b719781c7396
parent 55955 e8f1bf005661
child 56002 2028467b4df4