src/Pure/context.ML
changeset 11307 891fbd3f4881
parent 10924 92305ae9f460
child 11819 9283b3c11234