src/Pure/Syntax/ROOT.ML
changeset 21404 eb85850d3eb7
parent 15833 78109c7012ed