src/HOL/FunDef.thy
changeset 22270 4ccb7e6be929
parent 22268 ee2619267dca
child 22324 c95319d14332
equal deleted inserted replaced
22269:7c1e65897693 22270:4ccb7e6be929