src/Pure/envir.ML
changeset 13025 433c57d09d53
parent 12496 0a9bd5034e05
child 15531 08c8dad8e399