src/Pure/display.ML
changeset 7866 3ccaa11b6df9
parent 7635 4c1d2eb68db8
child 8402 84ff2d1f9a2c
equal deleted inserted replaced
7865:d9be8bc5624e 7866:3ccaa11b6df9