src/HOL/WF.thy
changeset 9444 13b10be222bf
parent 8882 9df44a4f1bf7