src/Pure/display.ML
changeset 39121 6f6a9c8abbac
parent 37248 8e8e5f9d1441
child 39050 600de0485859
equal deleted inserted replaced
39104:7430f17fd80e 39121:6f6a9c8abbac