src/Pure/envir.ML
changeset 39733 6d373e9dcb9d
parent 35408 b48ab741683b
child 42083 e1209fc7ecdc
equal deleted inserted replaced
39732:4dbc72759706 39733:6d373e9dcb9d