src/Pure/ML/ml_context.ML
changeset 57256 cf43583f9bb9
parent 56434 7acc933bd7cc
child 57832 5b48f2047c24