src/Pure/interpretation.ML
changeset 39811 0659e84bdc5f
parent 33522 737589bb9bb8
child 58177 166131276380
equal deleted inserted replaced
39810:5c9fe600525e 39811:0659e84bdc5f