src/HOL/Library/LaTeXsugar.thy
changeset 66912 a99a7cbf0fb5
parent 66527 7ca69030a2af
child 67386 998e01d6f8fd