src/HOL/WF.ML
changeset 6340 7d5cbd5819a0
parent 5579 32f99ca617b7
child 6433 228237ec56e5