src/Pure/ROOT.ML
changeset 10618 5b96bc5fbec3
parent 10413 0e015d9bea4e
child 10912 3cf3bb8ee324
equal deleted inserted replaced
10617:adc0ed64a120 10618:5b96bc5fbec3