src/HOL/FunDef.thy
changeset 20153 6ff5d35749b0
parent 19934 8190655ea2d4
child 20270 3abe7dae681e
equal deleted inserted replaced
20152:b6373fe199e1 20153:6ff5d35749b0