src/Pure/context.ML
changeset 11115 285b31e9e026
parent 10924 92305ae9f460
child 11819 9283b3c11234