Lines Matching defs:matches
219 val (matches,sups) = partition (curry op= (concl thm') o concl o (fn (a,b,c) => c)) s
220 fun ismatch (a,b,c) = mem (a,b,concl c) (map (fn (a,b,c) => (a,b,concl c)) matches)
221 val _ = if null matches then () else
226 trace 1 ("<<Encoding Messing>>: New rewrite matches other rewrites>>\n" ^ String.concat (map p sups))
330 (* instantiated such that t matches a disjunction, D, in P. Ie: *)
437 val matches = match thm_disjs term_disjs
441 (mapfilter (prove_term thm term) matches))
447 "<<Encoding Warning: Multiple matches in disjunction>>" ; x)
804 (* purposes as it allows tracking of partial matches. *)
808 (* As return_matches, except it matches a single rewrite. *)
887 val matches = Net.match term (!rewrites)
888 val _ = trace 3 (":" ^ int_to_string (length matches))
892 term o adjust)) matches
1311 (* If no rewrite matches a term then: *)
1409 let val matches = Net.match (lhs (snd (strip_imp (concl theorem)))) previous
1412 (aconv (concl theorem) (concl t))) matches
1445 | try_all_matches AE (match::matches) exns =
1448 (try_all_matches AE matches (exns @ L))
1451 | try_backchain_matches AE (ematch::matches) ((fails,assums),term) exns =
1454 handle Empty => try_backchain_matches AE matches
1456 | MatchFailure L => try_backchain_matches AE matches
1463 val (ematched,matches) = return_matches assums term
1468 case (matches @ cmatches)