src/HOL/ex/ROOT.ML
changeset 26229 116d3cfc0d89
parent 26104 200b4e401e65
child 26265 4b63b9e9b10d