Searched defs:pats (Results 1 - 16 of 16) sorted by relevance

/seL4-l4v-master/HOL4/tools/Holmake/tests/empty_script/
H A Dselftest.sml57 val pats = [["Couldn't find required output file:", "emptyTheory"], value
/seL4-l4v-master/HOL4/src/1/
H A Dmp_then.sml55 val pats = value
H A Dresolve_then.sml161 val pats = value
H A DHo_Rewrite.sml257 val pats = strip (concl th) value
H A DPmatch.sml692 val (pats,rhsides) = unzip clauses value
[all...]
H A DPrim_rec.sml1233 val pats = map (fn t => if is_imp t then rand t else t) cls value
/seL4-l4v-master/HOL4/src/coretypes/
H A DDefnBase.sml520 val pats = List.foldr foldthis [] patexps0 value
/seL4-l4v-master/HOL4/src/pfl/
H A Dindex.sml396 val (pats,rhsl) = unzip clauses value
/seL4-l4v-master/HOL4/src/q/
H A DQ.sml475 val pats = TermParse.prim_ctxt_termS Absyn (term_grammar()) ctxt q value
519 val pats = TermParse.prim_ctxt_termS Absyn (term_grammar()) fvs q value
[all...]
/seL4-l4v-master/HOL4/src/postkernel/
H A DHolKernel.sml700 val pats = map (Term.subst tmins) pats0 value
/seL4-l4v-master/HOL4/src/tfl/src/
H A DInduction.sml526 val (pats,TCsl) = unzip pat_TCs_list value
[all...]
H A DDefn.sml[all...]
/seL4-l4v-master/HOL4/src/num/termination/
H A DTotalDefn.sml358 val pats = mapfilter get_lhs (!termination_simps) value
/seL4-l4v-master/HOL4/src/emit/
H A DEmitML.sml767 val pats = clauses_to_patterns els value
/seL4-l4v-master/HOL4/examples/l3-machine-code/common/
H A DutilsLib.sml390 val pats = [``~ ~a: bool``, ``a /\ b``, ``~(a \/ b)``] value
/seL4-l4v-master/HOL4/src/pattern_matches/
H A DpatternMatchesLib.sml2732 val pats = List.map (#1 o dest_PMATCH_ROW) rows value
3082 val pats = List.map (#2 o dest_PMATCH_ROW_COND_EX) disjs value
[all...]

Completed in 133 milliseconds