src/Pure/envir.ML
changeset 72755 8dffbe01a3e1
parent 63619 9c870388e87a
child 74232 1091880266e5