src/Pure/context.ML
changeset 74525 c960bfcb91db
parent 74461 8e9f38240c05
child 74561 8e6c973003c8
equal deleted inserted replaced
74524:8ee3d5d3c1bf 74525:c960bfcb91db