src/Pure/envir.ML
changeset 23597 ab67175ca8a5
parent 22678 23963361278c
child 24670 9aae962b1d56
equal deleted inserted replaced
23596:f8381a95c49c 23597:ab67175ca8a5