src/HOL/Fun.thy
changeset 33756 47b7c9e0bf6e
parent 33318 ddd97d9dfbfb
child 34101 d689f0b33047
equal deleted inserted replaced
33755:6dc1b67f2127 33756:47b7c9e0bf6e