src/Pure/ROOT.ML
changeset 67516 656720e8f443
parent 67425 7d4a088dbc0e
child 67588 f3a68e350ab6
equal deleted inserted replaced
67515:fb87a0e9af21 67516:656720e8f443