src/HOL/Library/LaTeXsugar.thy
changeset 30549 d2d7874648bd
parent 30304 d8e4cd2ac2a1
child 30663 0b6aff7451b2
equal deleted inserted replaced
30548:2eef5e71edd6 30549:d2d7874648bd