src/HOL/WF.thy
changeset 1578 b58a6182e184
parent 1558 9c6ebfab4e05
child 3320 3a5e4930fb77