src/HOL/WF.ML
changeset 6980 bb526ba7ba5f
parent 6814 d96d4977f94e
child 7249 4886664d7033