src/HOL/ex/ROOT.ML
changeset 35595 1785d387627a
parent 35328 e8888458dce3
child 35950 791ce568d40a