src/HOL/WF.thy
changeset 2981 aa5aeb6467c6
parent 1558 9c6ebfab4e05
child 3320 3a5e4930fb77