src/Pure/Syntax/ROOT.ML
changeset 2495 82ec47e0a8d3
parent 2361 74c99949ad84
child 2691 d696d7e17046