src/HOL/WF.thy
changeset 9502 50ec59aff389
parent 8882 9df44a4f1bf7