src/HOL/ex/ROOT.ML
changeset 26898 0fffc7bc3604
parent 26265 4b63b9e9b10d
child 27421 7e458bd56860