new_recursive_definition : thm -> term -> thm
fn v1 ... (C1 vs1) ... vm = body1 /\ fn v1 ... (C2 vs2) ... vm = body2 /\ . . fn v1 ... (Cn vsn) ... vm = bodyn
`fn t1 ... v ... tm`
new_recursive_definition th ``;;
fn v1 ... (Ci vsi) ... vn
# let LIST_UNION = new_recursive_definition list_RECURSION `(LIST_UNION [] = {}) /\ (LIST_UNION (CONS h t) = h UNION (LIST_UNION t))`;; Warning: inventing type variables val ( LIST_UNION ) : thm = |- LIST_UNION [] = {} /\ LIST_UNION (CONS h t) = h UNION LIST_UNION t