src/HOL/Library/LaTeXsugar.thy
changeset 27263 a6b7f934fbc4
parent 25595 6c48275f9c76
child 27368 9f90ac19e32b