src/Pure/ML/ml_env.ML
changeset 59164 ff40c53d1af9
parent 59127 723b11f8ffbf
child 60746 8cf877aca29a
equal deleted inserted replaced
59163:857a600f0c94 59164:ff40c53d1af9