src/Pure/General/ROOT.ML
changeset 26845 d86eb226ecba
parent 26523 18ccad3ecb2e
child 26880 ebcd5c23dd96
equal deleted inserted replaced
26844:46b6306c181e 26845:d86eb226ecba