src/HOL/Library/Fin_Fun.thy
changeset 32608 c0056c2c1d17
parent 31804 627d142fce19
child 32657 5f13912245ff