src/Pure/envir.ML
changeset 23024 70435ffe077d
parent 22678 23963361278c
child 24670 9aae962b1d56
equal deleted inserted replaced
23023:7b52c4fde622 23024:70435ffe077d