src/HOL/WF.thy
changeset 8913 0bc13d5e60b8
parent 8882 9df44a4f1bf7