src/HOL/Fun.thy
changeset 21404 eb85850d3eb7
parent 21327 2b3c41d02e87
child 21547 9c9fdf4c2949