src/Pure/PIDE/resources.ML
changeset 64086 ac7ae5067783
parent 63675 e217525d6b64
child 65058 3e9f382fb67e
equal deleted inserted replaced
64085:1c451e5c145f 64086:ac7ae5067783