src/HOL/ex/ROOT.ML
changeset 19404 9bf2cdc9e8e8
parent 19281 b411f25fff25
child 19438 6d266e266b3f