Searched defs:matches (Results 1 - 19 of 19) sorted by relevance

/seL4-l4v-10.1.1/HOL4/src/postkernel/
H A DDB.sig27 val matches : term -> thm -> bool value
H A DDB.sml210 fun matches pat th = function
/seL4-l4v-10.1.1/HOL4/src/1/
H A DBoolExtractShared.sml310 val matches = (map mk_neg___idempot disj_matches) @ conj_matches; value
[all...]
H A Dmatch_goal.sml149 val matches = map (match_single fvs g o preprocess_matcher (HOLset.listItems fvs)) ms value
H A DTypeBasePure.sml693 val matches = List.mapPartial (check_match ty) matches0 value
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A DcongLib.sml120 val matches = Ho_Net.lookup term net; value
H A DsimpLib.sml427 val matches = Net.match lookup_t n value
/seL4-l4v-10.1.1/HOL4/examples/machine-code/garbage-collectors/
H A DboolTools.sml222 val matches = (map logical_mk_neg disj_matches) @ conj_matches; value
259 val matches = (map logical_mk_neg disj_t); value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/
H A Dcircuit-bisim.lisp
H A Dsummary.lisp
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DOverload.sml376 val matches = PrintMap.match(prmap, t) value
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/
H A Dtactics.sml467 let val matches = ONCE_DEPTH_USE_IMP_EQ_matches th gl; value
482 let val matches = ONCE_DEPTH_USE_IMP_matches th gl; value
/seL4-l4v-10.1.1/HOL4/examples/miller/subtypes/
H A DsubtypeTools.sml585 val matches = ovdiscrim_ho_match rules tm value
751 val matches = ovdiscrim_ho_match rewrs tm value
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/
H A DTYPEIDCODE.sml790 fun matches arg = mkEval(addPolymorphism(extractTest base), [arg]) function
/seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/
H A Dho_proverTools.sml875 val matches = ski_discrim_unify neg_db (vars, atom) value
890 val matches = ski_discrim_unify pos_db (vars, atom) value
/seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ParseTree/
H A DCODEGEN_PARSETREE.sml1250 val matches = map clauseToTree clauses value
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DDefn.sml1003 let fun matches (pat,_) = Lib.can (Term.match_term pat) function
/seL4-l4v-10.1.1/HOL4/examples/acl2/ml/
H A DfunctionEncodeLib.sml219 val (matches,sups) = partition (curry op= (concl thm') o concl o (fn (a,b,c) => c)) s value
437 val matches = match thm_disjs term_disjs value
887 val matches = Net.match term (!rewrites) value
1409 let val matches = Net.match (lhs (snd (strip_imp (concl theorem)))) previous value
[all...]
H A DpolytypicLib.sml3353 val matches = zip (map get_func htypes) htypes handle e => wrap e value
[all...]

Completed in 214 milliseconds