src/HOL/WF.ML
changeset 7360 7d3136b9af08
parent 7249 4886664d7033
child 7499 23e090051cb8