src/Pure/ROOT.ML
changeset 71046 b8aeeedf7e68
parent 70907 7e3f25a0cee4
child 71086 aedd11603fb4
equal deleted inserted replaced
71032:acedd04c1a42 71046:b8aeeedf7e68