src/Pure/ROOT.ML
changeset 1593 69ed69a9c32a
parent 1582 97a305db0c9e
child 1595 b9984b1dbc4c
equal deleted inserted replaced
1592:d89d5ff2397f 1593:69ed69a9c32a