src/HOL/WF.ML
changeset 5991 832ec852fc4e
parent 5579 32f99ca617b7
child 6433 228237ec56e5