src/HOL/Library/LaTeXsugar.thy
changeset 25459 d1dce7d0731c
parent 22328 cc403d881873
child 25467 bba589a88022