src/HOL/ex/ROOT.ML
changeset 47347 af937661e4a1
parent 47223 4fc34c628474
child 47474 214bfaae738d