src/Pure/envir.ML
changeset 53744 9db52ae90009
parent 52221 4ffe819a9b11
child 58945 cfb254e6c261
equal deleted inserted replaced
53743:87585d506db4 53744:9db52ae90009