src/HOL/Fun_Def.thy
changeset 57612 990ffb84489b
parent 56846 9df717fef2bb
child 57959 1bfed12a7646
equal deleted inserted replaced
57611:b6256ea3b7c5 57612:990ffb84489b