src/Pure/envir.ML
changeset 15298 a5bea99352d6
parent 12496 0a9bd5034e05
child 15531 08c8dad8e399
equal deleted inserted replaced
15297:0aff5d912422 15298:a5bea99352d6