src/HOL/ex/ROOT.ML
changeset 40417 a29b2fee592b
parent 40349 131cf8790a1c
child 40632 dc55e6752046