src/HOL/Library/Fin_Fun.thy
changeset 32739 31e75ad9ae17
parent 32657 5f13912245ff