src/HOL/WF.ML
changeset 5095 4436c62efceb
parent 5069 3ea049f7979d
child 5132 24f992a25adc