src/Pure/interpretation.ML
changeset 24854 0ebcd575d3c6
parent 24711 e8bba7723858
child 24857 2dde4189a055
equal deleted inserted replaced
24853:aab5798e5a33 24854:0ebcd575d3c6