src/HOL/Library/LaTeXsugar.thy
changeset 66717 67dbf5cdc056
parent 66527 7ca69030a2af
child 67386 998e01d6f8fd
equal deleted inserted replaced
66716:8737b866bd1c 66717:67dbf5cdc056