src/Pure/Syntax/ROOT.ML
changeset 17120 4ddeef83bd66
parent 15833 78109c7012ed
equal deleted inserted replaced
17119:b241ba3eb4db 17120:4ddeef83bd66