Lines Matching defs:conj
96 fun check_var var conj =
97 if is_eq conj then let
98 val (arg1, arg2) = dest_eq conj in
105 else if is_neg conj andalso dest_neg conj = var then false_tm
106 else if var = conj then truth_tm
200 fun CONJ_TO_FRONT_CONV conj term =
202 val (front,e,back) = split_at (term_eq conj) conjs
458 fun ELIM_EXISTS_CONV (var,conj) =
460 (CONJ_TO_FRONT_CONV conj THENC ENSURE_CONJ_CONV THENC
488 fun ELIM_FORALL_CONV (var,conj) =
490 (IMP_TO_FRONT_CONV conj THENC LAND_CONV (ENSURE_EQ_CONV var)))
504 let val (conj,value) = find_var_value (hd vars) (strip_conj body)
507 THENC LAST_EXISTS_CONV (ELIM_EXISTS_CONV (hd vars,conj))) tm