src/Pure/envir.ML
changeset 7505 a9690e9cc58a
parent 5289 41b949f3b8ac
child 8407 d522ad1809e9
equal deleted inserted replaced
7504:0fec51813079 7505:a9690e9cc58a