src/HOL/Library/Fin_Fun.thy
changeset 32685 29e4e567b5f4
parent 31804 627d142fce19
child 32657 5f13912245ff