src/HOL/WF.ML
changeset 9789 7e5e6c47c0b5
parent 9422 4b6bc2b347e5
child 9970 dfe4747c8318