src/Pure/Syntax/ROOT.ML
changeset 18800 c0f90bbf3865
parent 15833 78109c7012ed