Lines Matching refs:count
619 ought to solve the goal. The count parameters keeps track of what
625 fun mk_more_tactics num_hyps count (hyp1::hyps) =
627 fun mk_still_more_tactics count =
628 if count < num_rules + num_hyps then
630 let val rule_thm = ASSUME (nth (rev asms, count))
633 end)::mk_still_more_tactics (count + 1)
642 let val rule_thm = ASSUME (nth (rev asms, count))
650 end::mk_more_tactics num_hyps (count + 1) hyps
653 fun mk_tactics count (rule::rules) =
667 (mk_tactics (count + 1) rules)
670 let val rule_thm = ASSUME (nth (rev asms, hyp_count + count))
678 end)::(mk_tactics (count + 1) rules)
696 fun mk_prop_vars count (rel::rels) =
697 mk_var ("P_"^(Lib.int_to_string count),
698 snd (dest_var rel)) :: mk_prop_vars (count + 1) rels
1128 fun assemble_preds count (pred::more_preds) (rel::more_rels) =
1129 if count = 0 then
1130 pred::(assemble_preds (count - 1) more_preds more_rels)
1132 rel::(assemble_preds (count - 1) more_preds more_rels)
1133 | assemble_preds count _ _ = []
1379 fun mk_inversion_thms count all_rels (hyp::hyps) (vars::more_vars) =
1380 let val new_preds = assemble_preds count preds all_rels
1381 val rel = nth (all_rels, count)
1391 (UNDISCH (nth (CONJUNCTS (UNDISCH thm1), count)))
1406 val conjs = flatten (elim_nth count divided_conjs)
1407 val rules = flatten (elim_nth count divided_rules)
1415 val relevant_rules = nth (divided_rules, count)
1435 (mk_inversion_thms (count + 1) all_rels hyps more_vars)
1442 (* fun mk_inversion_thms count all_rels (hyp::hyps) (vars::more_vars) = *)