src/Pure/envir.ML
changeset 30266 970bf4f594c9
parent 30146 a77fc0209723
child 32018 3370cea95387
equal deleted inserted replaced
30265:2ec2df1a1665 30266:970bf4f594c9