| /seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
| H A D | arm_parserLib.sml | 712 let val n1 = uint_of_word tm1 value
|
| /seL4-l4v-10.1.1/HOL4/examples/CCS/ |
| H A D | StrongLawsConv.sml | 318 and [n1, n2] = map (term_of_int o length) [ls1, ls2]; value
|
| /seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/ |
| H A D | decidable_separationLogicLib.sml | 894 val n1 = valOf (find_entry 0 e1 cL); value
1478 val (n1,n2,e1,e2) = find_strengthen_eq_pair cL pfL handle _ => value
1493 val n1 = valOf (find_entry 0 e1 cL1); value
1511 val (n1,n2,e1,e2) = find_strengthen_eq_precondition cL1 cL2 handle _ => value
1647 val (n1, n2, n3, turn, e1, e2,e3, f, a) = valOf searchOpt; value
1918 val (n1, sf) = valOf (find_in_list (fn sf => (let val (f', e1', e2') = dest_sf_ls sf in (f = f') andalso (e1' = e1) end)) sfL); value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | mechReasoning.sml | 1606 val (n1, n2) = (Arbnum.divmod (n, Arbnum.fromInt 4)) value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | mechReasoning.sml | 1054 val (n1, n2) = (Arbnum.divmod (n, Arbnum.fromInt 4)) value
|
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/c_output/ |
| H A D | c_outputLib.sml | 684 val n1 = Arbnum.fromInt (el 1 l); value
|
| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/ |
| H A D | separationLogicLib.sml | 868 val (n1, thm0_opt) = sys [] context 0 dir body; value
|
| H A D | vars_as_resourceBaseFunctor.sml | 580 val (n1, n2, turn, _, _, _, _) = valOf foundOpt value
|
| H A D | vars_as_resourceFunctor.sml | 3887 val (n1, thm1_opt) = mc step_opt t; value
|
| /seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
| H A D | realconv.cpp | 1041 int i, k1, n, n1; variable
|
| /seL4-l4v-10.1.1/HOL4/src/0/ |
| H A D | Term.sml | 862 let val n1 = id_toString c1 value
|
| H A D | Type.sml | 268 else let val n1 = KernelSig.id_toString (fst c1) value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | ConseqConv.sml | 542 val (n1, thm1) = check_sys_call sys [] context 0 dir b1; value
566 val (n1, thm1) = check_sys_call sys [] context 0 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1; value
598 val (n1, thm1_opt) = sys [b2] context 0 dir b1; value
622 val (n1, thm1_opt) = sys [] context 0 dir b1; value
662 val (n1, thm1_op value
685 val (n1, thm1_opt) = sys [] context 0 dir b1; value
726 val (n1, thm1_opt) = sys [a1] context 0 dir b2; value
749 val (n1, thm1_opt) = sys [] context 0 dir b2; value
769 val (n1, thm1_opt) = sys [] context 0 (CONSEQ_CONV_DIRECTION_NEGATE dir) b1; value
815 val (n1, thm1_opt) = sys [] context 0 dir b1; value
832 val (n1, thm1_opt) = sys [c] context 0 dir b1; value
859 val (n1, thm1_opt) = sys [] (var_filter_context v context) 0 dir b1; value
872 val (n1, thm1_opt) = sys [] (var_filter_context v context) 0 dir b1; value
[all...] |
| H A D | Drule.sml | 1461 val n1 = fst (dest_var v1) value
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/ |
| H A D | def_cnf.sml | 90 let val (n1,v1,defs1,lfn1) = localdefs cnfv (rand tm) (n,defs,lfn) value
98 let val (n1,v1,defs1,lfn1) = localdefs cnfv (land tm) (n,defs,lfn) value
108 val (n1,v1,defs1,lfn1) = localdefs cnfv (List.nth(args,0)) (n,defs,lfn) value
118 handle NotFound => let val n1 = n + 1 value
128 handle NotFound => let val n1 = n + 1 value
134 let val (n1,tm1,vdefs1,lfn1) = transvar_var cnfv (n,rand tm,vdefs,lfn) value
144 let val (n1,p1,vdefs1,lfn1) = transvar_lit cnfv (n,p,vdefs,lfn) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
| H A D | Yices.sml | 351 let val (n1, n2, w, dim_ty) = wordsSyntax.dest_word_extract tm value
352 val n1 = numSyntax.dest_numeral n1 value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/compute/examples/ |
| H A D | MergeSort.sml | 73 val n1 = --`SUC 0 `--; value
[all...] |
| H A D | Sort.sml | 36 val n1 = S O; value
|
| /seL4-l4v-10.1.1/HOL4/src/list/src/ |
| H A D | listSimps.sml | 183 val n1 = length L1 value
253 val n1 = length L1 value
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibMeson.sml | 153 fun halves n = let val n1 = n div 2 in (n1, n - n1) end; value
511 val (n1, n2) = halves n value
|
| /seL4-l4v-10.1.1/HOL4/src/n-bit/ |
| H A D | wordsSyntax.sml | 383 val (n1, n2, s) = HolKernel.dest_triop tm1 e w value
397 val (n1, n2, w1) = HolKernel.dest_triop tm1 e w value
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | term_grammar.sml | |
| /seL4-l4v-10.1.1/HOL4/src/portableML/ |
| H A D | Arbrat.sml | 40 fun (n1, d1) + (n2, d2) = function
45 fun (n1, d1) * (n2, d2) = norm (Arbint.* (n1, n2), Arbnum.* (d1, d2)) function
64 fun (n1, d1) < (n2, d2) = function
|
| /seL4-l4v-10.1.1/HOL4/src/real/ |
| H A D | RealArith.sml | 1065 val (n1,n2) = value
|
| /seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/ |
| H A D | schorr_waite.c | 90 struct node n1[max_size], n2[max_size]; local
[all...] |