src/Pure/context.ML
changeset 72047 b9e9ff3a1e1c
parent 70586 57df8a85317a
child 72060 efb7fd4a6d1f
equal deleted inserted replaced
72046:c386d1b77762 72047:b9e9ff3a1e1c