src/HOL/Library/FinFun.thy
changeset 50972 d2c6a0a7fcdf
parent 49834 b27bbb021df1
child 51124 8fd094d5b7b7