src/HOL/WF.thy
changeset 1868 836950047d85
parent 1558 9c6ebfab4e05
child 3320 3a5e4930fb77