src/HOL/ex/ROOT.ML
changeset 26157 4d9d0a26c32a
parent 26104 200b4e401e65
child 26265 4b63b9e9b10d