src/HOL/FunDef.thy
changeset 20157 28638d2a6bc7
parent 19934 8190655ea2d4
child 20270 3abe7dae681e
equal deleted inserted replaced
20156:7a7898b1cfa4 20157:28638d2a6bc7