src/HOL/WF.ML
changeset 5553 ae42b36a50c2
parent 5521 7970832271cc
child 5579 32f99ca617b7