src/HOL/Library/ROOT.ML
changeset 47197 ed681ca1188a
parent 47108 2a1953f0d20d
child 47232 e2f0176149d0