src/HOL/Fun.thy
changeset 15130 dc6be28d7f4e
parent 15111 c108189645f8
child 15131 c69542757a4d
equal deleted inserted replaced
15129:fbf90acc5bf4 15130:dc6be28d7f4e