equal
deleted
inserted
replaced
335 (*Does t occur in u? Or is alpha-convertible to u? |
335 (*Does t occur in u? Or is alpha-convertible to u? |
336 The term t must contain no loose bound variables*) |
336 The term t must contain no loose bound variables*) |
337 fun occs (t, u) = exists_subterm (fn s => t aconv s) u; |
337 fun occs (t, u) = exists_subterm (fn s => t aconv s) u; |
338 |
338 |
339 (*Close up a formula over all free variables by quantification*) |
339 (*Close up a formula over all free variables by quantification*) |
340 fun close_form A = |
340 fun close_form A = fold (all o Free) (Term.add_frees A []) A; |
341 Term.list_all_free (rev (Term.add_frees A []), A); |
|
342 |
341 |
343 |
342 |
344 |
343 |
345 (*** Specialized operations for resolution... ***) |
344 (*** Specialized operations for resolution... ***) |
346 |
345 |