src/Pure/context.ML
changeset 74740 d14918fcbd37
parent 74561 8e6c973003c8
child 77693 068ff989c143
equal deleted inserted replaced
74739:a06652d397a7 74740:d14918fcbd37