src/Pure/context.ML
changeset 31343 9983f648f9bb
parent 30628 4078276bcace
child 31971 8c1b845ed105