src/HOL/Fun.thy
changeset 12397 6766aa05e4eb
parent 12338 de0f4a63baa5
child 12459 6978ab7cac64
equal deleted inserted replaced
12396:2298d5b8e530 12397:6766aa05e4eb