src/HOL/Library/LaTeXsugar.thy
changeset 55359 2d8222c76020
parent 55114 0ee5c17f2207
child 55954 a29aefc88c8d
equal deleted inserted replaced
55357:1dd39517e1ce 55359:2d8222c76020