equal
deleted
inserted
replaced
423 (*Does t occur in u? Or is alpha-convertible to u? |
423 (*Does t occur in u? Or is alpha-convertible to u? |
424 The term t must contain no loose bound variables*) |
424 The term t must contain no loose bound variables*) |
425 fun occs (t, u) = exists_subterm (fn s => t aconv s) u; |
425 fun occs (t, u) = exists_subterm (fn s => t aconv s) u; |
426 |
426 |
427 (*Close up a formula over all free variables by quantification*) |
427 (*Close up a formula over all free variables by quantification*) |
428 fun close_form A = fold (all o Free) (Term.add_frees A []) A; |
428 fun close_form A = |
|
429 fold_rev (all o Free) (Frees.build (Frees.add_frees A) |> Frees.list_set) A; |
429 |
430 |
430 |
431 |
431 |
432 |
432 (*** Specialized operations for resolution... ***) |
433 (*** Specialized operations for resolution... ***) |
433 |
434 |