/seL4-l4v-master/HOL4/examples/elliptic/c_output/ |
H A D | c_outputLibExamples.sml | 29 val defs = [ex1_field_neg_alt, ex1_field_add_alt, ex1_field_sub_alt, value
|
H A D | c_outputLib.sml | [all...] |
/seL4-l4v-master/HOL4/src/opentheory/postbool/ |
H A D | loggingHolKernel.sml | |
H A D | Logging.sml | 336 val defs = th2 :: defs value
|
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/ |
H A D | elliptic.751.sml | 206 val defs = [field_neg_def, field_add_def, field_sub_def, field_mult_aux_def] value
|
/seL4-l4v-master/HOL4/src/HolSat/vector_def_CNF/ |
H A D | defCNF.sml | 57 val (defs, a) = f defs a value 58 val (defs, b) = f defs b value 147 val (defs, tm') = conj_cnf ((!dcnfgv)(), zero, []) tm value [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/x64_compiler/ |
H A D | x64_compilerLib.sml | 117 val defs = map (fn (x,y,z) => y) xs value
|
/seL4-l4v-master/HOL4/src/HolSmt/ |
H A D | Yices.sml | 691 val defs = "(define " ^ name ^ "::" ^ ty_name ^ ")" :: defs value 759 val defs = List.map (fn s => s ^ "\\n") (List.rev defs) value [all...] |
/seL4-l4v-master/HOL4/src/emit/ |
H A D | extended_emitScript.sml | 112 val defs = value 191 val defs = map DEFN [dividesTheory.compute_divides, GCD_EFFICIENTLY, lcm_def]; value 325 val defs = value 387 val defs value [all...] |
H A D | basis_emitScript.sml | 13 val defs = map DEFN [S_THM, K_THM, I_THM, W_THM, C_THM, o_THM, APPLY_UPDATE_THM] value 20 val defs = value 72 val defs = map DEFN value 419 val defs value 509 val defs = value 529 val defs = value 591 val defs = value 689 val defs = value 731 val defs = value 852 val defs = value 903 val defs = value 1061 val defs = value 1109 val defs = [SUMi, MULi, EXPi, dimindexi, mk_fcp_def, index_comp, fcp_subst_comp] value 1241 fun defs ocaml = function 1504 val defs = value [all...] |
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | flookupLib.sml | 236 val defs = iter [] x value
|
/seL4-l4v-master/HOL4/src/ring/src/ |
H A D | abstraction.sml | 211 val defs = List.mapPartial mk_def ctab value 267 val defs = rev (map fst (definitions"-")) value
|
/seL4-l4v-master/HOL4/examples/dev/sw2/ |
H A D | defunctionalize.sml | 560 val defs = [empty_def, member_def, insert_def, upto_def]; value 600 val defs = [f_def, g_def, k_def]; value [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/acl2/ |
H A D | m1_progScript.sml | 299 val defs = map acl2_simp [actual_defun, app_defun, arg1_defun, value
|
/seL4-l4v-master/HOL4/examples/machine-code/compiler/ |
H A D | compilerLib.sml | 123 val defs = map (fn (x,y,z) => y) xs value 170 val defs = f (map (fn (x,y,z) => y) xs) value
|
/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | annotatedIR.sml | 659 val defs = List.map (fn (name, (flag,src,anf,cps)) => src) env; value
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | annotatedIR.sml | 602 val defs = List.map (fn (name, (flag,src,anf,cps)) => src) env; value
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | annotatedIR.sml | 602 val defs = List.map (fn (name, (flag,src,anf,cps)) => src) env; value
|
/seL4-l4v-master/HOL4/src/datatype/ |
H A D | EnumType.sml | 248 val defs = map (new_definition o def) nclist value [all...] |
/seL4-l4v-master/HOL4/src/IndDef/ |
H A D | InductiveDefinition.sml | 590 let val (defs,others) = partition is_eq (hyp th) value 612 val defs = filter is_eq (hyp th) value
|
/seL4-l4v-master/HOL4/src/temporal/src/ |
H A D | temporalLib.sml | 385 let val (defs,phi') = tableau phi value 417 val (defs,phi') = tableau phi value 430 val (defs,phi') = tableau phi value 439 val (defs,phi') = tableau phi value 508 val (defs,phi') = tableau phi value 517 val (defs,phi') = tableau phi value 526 val (defs,phi') = tableau phi value 535 val (defs,phi') = tableau phi value 752 val (defs,pt) = tableau tt value 816 val (defs,pt) = tableau tt value 935 val defs = tl restlist value 1012 val defs = tl restlist value [all...] |
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_extractLib.sml | 549 val defs = map define_parts (zip data rs) value
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | normalForms.sml | 736 val (defs, a) = f defs a value 737 val (defs, b) = f defs b value 785 val (defs, tm) = conj_cnf [] tm value 794 val (defs, tm) = gen_def_cnf tm value 1149 val defs = (def_tm,(vs,tm,def)) :: defs value 1170 val (defs,vs,tm,def,def_th) = mk_def defs vs tm value 1367 val (defs,rule,dth) = rename defs vs tm value 1380 val defs = [] value 1381 val (defs,ths) = min_cnf_prep defs [] ths value 1382 val (defs,ths) = min_cnf_norm defs [] ths value [all...] |
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | lisp_parseScript.sml | 2375 val defs = map mk_func tts value 2390 val defs = map mk_func2 tts value
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | automationLib.sml | 426 val defs = def |> CONJUNCTS |> map SPEC_ALL value 439 val defs = preprocess_def def value
|