src/HOL/Fun.thy
changeset 21404 eb85850d3eb7
parent 21327 2b3c41d02e87
child 21547 9c9fdf4c2949
equal deleted inserted replaced
21403:dd58f13a8eb4 21404:eb85850d3eb7