src/HOL/Library/LaTeXsugar.thy
changeset 26057 f5d5c4922cdf
parent 25595 6c48275f9c76
child 27368 9f90ac19e32b
equal deleted inserted replaced
26056:6a0801279f4c 26057:f5d5c4922cdf