src/HOL/Library/ROOT.ML
changeset 45873 37ffb8797a63
parent 45483 34d07cf7d207
child 45985 2d399a776de2
equal deleted inserted replaced
45872:3759fb8a02b8 45873:37ffb8797a63