| /seL4-l4v-master/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibParameters.sml | 108 val t1 = pairSyntax.mk_fst v; value
402 val conj_lift_qp = dest_lift_qp (fn t => (let val (t1,t2) = dest_conj t in [t1, t2] end)) value
|
| H A D | quantHeuristicsTools.sml | 77 val (t1, t23) = dest_imp t value
119 val (t1, t2) = dest_imp (concl thm) value
133 val (t1, t2) = dest_imp (concl thm) value
147 val (t1, t2) = dest_imp (concl thm) value
161 val (t1, t2) = dest_imp (concl thm) value
284 val (t1,t2) = dest_disj (dest_neg t); value
291 val (t1,t2) = dest_conj (dest_neg t); value
299 val (t1,t2) = dest_conj t; value
306 val (t1,t2) = dest_disj t; value
472 val (t1,t2) = dest_conj t; value
480 val (t1,t2) = dest_disj_imp t; value
488 val t1 = dest_neg t; value
520 val t1 = subst_occs [[1]] [org_rw_term |-> dummy_var] t value
[all...] |
| /seL4-l4v-master/seL4/include/arch/riscv/arch/machine/ |
| H A D | registerset.h | 31 t1 = 5, enumerator in enum:_register
|
| /seL4-l4v-master/HOL4/src/HolSmt/ |
| H A D | Yices.sml | 300 let val (t1, t2, t3) = boolSyntax.dest_bool_case tm value
310 let val t1 = pairSyntax.dest_fst tm value
318 let val t1 = pairSyntax.dest_snd tm value
338 let val (t1, num) = wordsSyntax.dest_index tm value
393 let val (t1, dim_ty) = wordsSyntax.dest_w2w tm value
414 let val (t1, dim_ty) = wordsSyntax.dest_sw2sw tm value
435 let val t1 = wordsSyntax.dest_word_msb tm value
671 let val (t1, t2) = Term.dest_comb tm value
[all...] |
| /seL4-l4v-master/HOL4/examples/dev/sw/ |
| H A D | ANF.sml | 135 then let val (t1,t2) = dest_pair t value
213 val (t1,t2) = dest_comb(rhs(concl th0)) value
[all...] |
| H A D | regAllocation.sml | 895 let val (t1,t2) = dest_pair exp value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
| H A D | ANF.sml | 135 then let val (t1,t2) = dest_pair t value
213 val (t1,t2) = dest_comb(rhs(concl th0)) value
[all...] |
| H A D | regAllocation.sml | 895 let val (t1,t2) = dest_pair exp value
|
| /seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
| H A D | ANF.sml | 135 then let val (t1,t2) = dest_pair t value
213 val (t1,t2) = dest_comb(rhs(concl th0)) value
[all...] |
| H A D | regAllocation.sml | 895 let val (t1,t2) = dest_pair exp value
|
| /seL4-l4v-master/HOL4/examples/elliptic/ |
| H A D | Map.sml | 259 val (t1,t2) = treeCombineRemove cmp f t1 t2 value
[all...] |
| /seL4-l4v-master/HOL4/src/bag/ |
| H A D | bagSimpleLib.sml | 119 val t1 = mk_image (f, b1) value
521 val (t1,t2) = dest_eq t; value
|
| /seL4-l4v-master/HOL4/src/floating-point/ |
| H A D | binary_ieeeSyntax.sml | 127 val (t1, t2) = value
139 val t1 = wordsSyntax.mk_wordii (i, w) value
|
| /seL4-l4v-master/HOL4/src/parse/ |
| H A D | Absyn.sml | 101 fun binAQ f x locn err = let val (t1,t2) = f x value
|
| /seL4-l4v-master/HOL4/src/res_quan/src/ |
| H A D | res_quanLib.sml | 477 let val (t1,t2) = pairSyntax.dest_pair tm value
502 let val (t1,t2) = dest_comb tm value
[all...] |
| /seL4-l4v-master/HOL4/examples/HolBdd/ |
| H A D | MachineTransitionScript.sml | 625 val t1 = SELECT_RULE(EQ_MP (SPEC (``r:'a``) asm2) value
|
| /seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
| H A D | boolTools.sml | 73 (let val (t1,t2)=dest_disj t; value
81 (let val (t1,t2)=dest_conj t; value
94 (let val (t1,t2)=dest_imp t; value
332 val (t1, t2) = dest_imp thm_term; value
[all...] |
| /seL4-l4v-master/HOL4/examples/formal-languages/regular/ |
| H A D | regexpLib.sml | 273 val [t1,t2,t3] = strip_pair triple value
|
| /seL4-l4v-master/HOL4/src/real/ |
| H A D | realSyntax.sml | 99 val (t1, t2) = dest_plus t value
124 val (t1, t2) = dest_mult t value
[all...] |
| /seL4-l4v-master/HOL4/src/num/arith/src/ |
| H A D | numSimps.sml | 235 let val (t1,t2) = dest_plus tm value
241 let val (t1,t2) = dest_minus tm value
255 let val (t1, t2) = dest_mult tm value
422 val (t1,t2,t3) = (hd args, hd (tl args), hd (tl (tl args))) value
434 val (t1, t2) = (hd args, hd (tl args)) value
[all...] |
| /seL4-l4v-master/HOL4/src/pattern_matches/ |
| H A D | patternMatchesSyntax.sml | 68 val (t1, t2) = dest_disj t value
232 val (t1, t2) = dest_comb t value
428 val t1 = mk_comb (b_tm, v) value
729 val t1 = mk_comb (b_tm, v) value
[all...] |
| /seL4-l4v-master/HOL4/src/datatype/ |
| H A D | DatatypeSimps.sml | 106 val t1 = foldl (fn ((args, _), t) => value
168 val t1 = list_mk_icomb (c', args) value
206 val t1 = list_mk_icomb (case_c, [input_arg] @ case_args0) value
242 val t1 = list_mk_icomb (case_c, [input_arg] @ case_args0) value
278 val t1 = list_mk_icomb (case_c, [input_arg] @ case_args0) value
[all...] |
| /seL4-l4v-master/HOL4/src/integer/ |
| H A D | OmegaMath.sml | 696 val t1 = hd (strip_plus (rand g)) value
|
| /seL4-l4v-master/HOL4/src/pfl/ |
| H A D | index.sml | |
| /seL4-l4v-master/HOL4/src/quotient/examples/ |
| H A D | tactics.sml | 183 let val (t1,t2) = dest_eq gl; value
191 let val (t1,t2) = dest_eq gl; value
[all...] |