src/HOL/WF.ML
changeset 8771 026f37a86ea7
parent 8703 816d8f6513be
child 9108 9fff97d29837