src/HOL/ex/ROOT.ML
changeset 26402 441ddf3b8f02
parent 26265 4b63b9e9b10d
child 27421 7e458bd56860