Lines Matching refs:clause
705 of SOME (var_list,clause) => raise (dexn ("The variables; " ^ xlist_to_string term_to_string var_list ^
706 " are free in the clause: " ^ term_to_string clause))
881 (* a) there can be no free variables in any clause except fni *)
889 (* a) there can be no free variables in any clause except fni *)
1016 fun conv clause =
1019 (op:: (strip_comb (rand (lhs (snd (strip_forall clause))))))
1023 clause
1189 fun is_double_term_target (scheme:translation_scheme) funcs clause term =
1199 (is_single_constructor scheme clause orelse is_lr_term x) handle e => wrapException "is_double_term_target" e
1203 fun is_double_term_source funcs (clause:term) term =
1456 [("x is free in the function body, should be either R x or L x, in function clause:\n" ^
1741 (* Given theorems of the form: [..] |- Pi (f x) ==> Pj (f x) and a clause, *)
1743 fun fix_thms [] clause induction = raise Empty
1744 | fix_thms thms clause induction =
1745 let val (ante,conc) = (dest_imp_only o snd o strip_forall) clause
1759 (* Finds all terms in the clause such that there is a function call: *)
1763 fun check_replace clause induction =
1764 let val pred = guarenteed (rator o snd o dest_imp_only o snd o strip_forall) clause
1772 fix_thms rv clause induction
3610 curry op^ ("Could not prove the clause:\n" ^