src/HOL/Fun.thy
changeset 33446 153a27370a42
parent 33318 ddd97d9dfbfb
child 34101 d689f0b33047
equal deleted inserted replaced
33445:f0c78a28e18e 33446:153a27370a42