src/HOL/WF.ML
changeset 5526 e7617b57a3e6
parent 5521 7970832271cc
child 5579 32f99ca617b7