| /seL4-l4v-master/HOL4/src/res_quan/src/ |
| H A D | res_quanLib.sml | 481 val l2 = check_varstruct t2 value
504 val l2 = check_varstruct t2 value
|
| /seL4-l4v-master/HOL4/examples/HolCheck/ |
| H A D | commonTools.sml | 194 val l2 = if (is_cond f2) then depth_dest_cond_aux (dest_cond f2) else [] value
206 val l2 = if (is_cond f2) then gen_dest_cond_aux (dest_cond f2) else [([],f2)] value
|
| H A D | muSyntax.sml | 401 val l2 = List.filter (fn t => List.null (fv t)) l1 value
402 val l2 = List.map mk_hol_proxy l2 value
|
| /seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
| H A D | boolTools.sml | [all...] |
| H A D | lisp_gcScript.sml | 2500 val l2 = prove_eq "x86_move2" "arm_move2" [] value
2525 val l2 = prove_eq "ppc_move2" "arm_move2" [] value
[all...] |
| /seL4-l4v-master/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsTools.sml | 474 val (l2,_) = crw_strip crw_conj t2; value
482 val (l2,_) = crw_strip crw_disj t2; value
|
| /seL4-l4v-master/HOL4/src/AI/proof_search/ |
| H A D | psMCTS.sml | 273 val l2 = dict_sort compare_rmax l1 value
|
| /seL4-l4v-master/HOL4/src/real/ |
| H A D | realaxScript.sml | 158 val l2 = mk l' value
|
| H A D | RealArith.sml | 639 val (l2,r2) = dest tm2 value
699 val (l2,r2) = dest tm2 value
[all...] |
| /seL4-l4v-master/HOL4/src/num/arith/src/ |
| H A D | numSimps.sml | 237 val (l2,k2) = dest_lin(lin_of_term t2) value
243 val (l2,k2) = dest_lin(lin_of_term t2) value
|
| /seL4-l4v-master/HOL4/src/list/src/ |
| H A D | ListConv1.sml | 232 val l2 = fst(dest_list rhs) value
[all...] |
| /seL4-l4v-master/HOL4/src/metis/ |
| H A D | mlibMeson.sml | 199 val (l2, l3) = divide l' n value
|
| /seL4-l4v-master/HOL4/src/pfl/ |
| H A D | index.sml | 93 and l2 = FILTER (\\x. x > h) t value
[all...] |
| /seL4-l4v-master/HOL4/examples/ARM_security_properties/ |
| H A D | switching_lemmaScript.sml | 984 val l2 = ``(constT () value
|
| /seL4-l4v-master/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | reorder.c | 1524 int l1, l2; local
|
| /seL4-l4v-master/HOL4/examples/separationLogic/src/ |
| H A D | separationLogicLib.sml | 525 val l2 = mk_list_term x2 a2 value
|
| /seL4-l4v-master/HOL4/examples/l3-machine-code/common/ |
| H A D | core_decompilerLib.sml | 488 val l2 = ref TRUTH value
|
| H A D | stateLib.sml | 825 val l2 = List.map (I ## mk_footprint1 syntax1) l2 value
844 val l2 = List.map d (not_in_asserts p c l) value
[all...] |
| /seL4-l4v-master/HOL4/src/tactictoe/src/ |
| H A D | tttSearch.sml | 219 val l2 = dict_sort compare_rmax l1 value
|
| /seL4-l4v-master/HOL4/src/AI/ |
| H A D | aiLib.sml | 920 val l2 = map rm_last_char l1 (* removing end line *) value
934 val l2 = map rm_last_char l1 (* removing end line *) value
[all...] |
| /seL4-l4v-master/HOL4/examples/l3-machine-code/m0/prog/ |
| H A D | m0_progLib.sml | 442 val l2 = List.drop (l, 16) value
|
| /seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
| H A D | CODETREE_OPTIMISER.sml | 350 val l1 = length n1 and l2 = length n2 value
|
| /seL4-l4v-master/HOL4/examples/decidable_separationLogic/src/ |
| H A D | decidable_separationLogicLib.sml | 529 val l2 = map (fn sf => (should_turn (dest_eq_uneq sf) handle _ => false)) pfL'; value
564 val l2 = rev l1; value
[all...] |
| /seL4-l4v-master/HOL4/examples/l3-machine-code/m0/step/ |
| H A D | m0_stepLib.sml | 901 val l2 = mk_bool_list (List.drop (l, 16)) value
|
| /seL4-l4v-master/HOL4/examples/machine-code/decompiler/ |
| H A D | decompilerLib.sml | 1777 val l2 = CONV_RULE (RAND_CONV (PRE_CONV (fix_star xi) THENC value
1780 val l2 = GEN_TUPLE x_in (GEN_TUPLE new_input l2) handle HOL_ERR _ => l2 value
[all...] |