src/Pure/Syntax/ROOT.ML
changeset 6109 82b50115564c
parent 5683 e62518aacc5b
child 6116 8ba2f25610f7