src/Pure/ROOT.ML
changeset 1444 23ceb1dc9755
parent 1443 ff8a804e0201
child 1498 7b7d20e89b1b
equal deleted inserted replaced
1443:ff8a804e0201 1444:23ceb1dc9755