src/Pure/envir.ML
changeset 12970 c9b1838a2cc0
parent 12496 0a9bd5034e05
child 15531 08c8dad8e399