src/Pure/ROOT.ML
changeset 70867 4c8e28dabbc4
parent 70784 799437173553
child 70893 ce1e27dcc9f4
equal deleted inserted replaced
70866:209327bd3e3e 70867:4c8e28dabbc4