src/Pure/context.ML
changeset 69510 0f31dd2e540d
parent 68482 cb84beb84ca9
child 70360 03430649a7d2