src/HOL/Library/FinFun.thy
changeset 63414 beb987127d0f
parent 63283 a59801b7f125