src/HOL/Lfp.thy
changeset 15485 e93a3badc2bc
parent 15386 06757406d8cf