src/HOL/ex/ROOT.ML
changeset 37087 dd47971b9875
parent 36962 5fb251d1c32f
child 37280 0fb011773adc