src/HOL/Fun_Def.thy
changeset 58732 854eed6e5aed
parent 58377 c6f93b8d2d8e
child 58819 aa43c6f05bca
equal deleted inserted replaced
58731:43a3ef574065 58732:854eed6e5aed