src/HOL/WF.ML
changeset 9369 139fde7af7bd
parent 9181 25f993973fac
child 9422 4b6bc2b347e5