src/Pure/ML/ml_context.ML
changeset 56604 1b153b989860
parent 56434 7acc933bd7cc
child 57832 5b48f2047c24