src/HOL/FunDef.thy
changeset 38826 f42f425edf24
parent 37767 a2b7a20d6ea3
child 40108 dbab949c2717
equal deleted inserted replaced
38825:4ec3cbd95f25 38826:f42f425edf24