Searched defs:defs (Results 1 - 25 of 36) sorted by relevance

12

/seL4-l4v-master/HOL4/examples/elliptic/c_output/
H A Dc_outputLibExamples.sml29 val defs = [ex1_field_neg_alt, ex1_field_add_alt, ex1_field_sub_alt, value
H A Dc_outputLib.sml[all...]
/seL4-l4v-master/HOL4/src/opentheory/postbool/
H A DloggingHolKernel.sml
H A DLogging.sml336 val defs = th2 :: defs value
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/
H A Delliptic.751.sml206 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 DdefCNF.sml57 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 Dx64_compilerLib.sml117 val defs = map (fn (x,y,z) => y) xs value
/seL4-l4v-master/HOL4/src/HolSmt/
H A DYices.sml691 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 Dextended_emitScript.sml112 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 Dbasis_emitScript.sml13 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 DflookupLib.sml236 val defs = iter [] x value
/seL4-l4v-master/HOL4/src/ring/src/
H A Dabstraction.sml211 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 Ddefunctionalize.sml560 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 Dm1_progScript.sml299 val defs = map acl2_simp [actual_defun, app_defun, arg1_defun, value
/seL4-l4v-master/HOL4/examples/machine-code/compiler/
H A DcompilerLib.sml123 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 DannotatedIR.sml659 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 DannotatedIR.sml602 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 DannotatedIR.sml602 val defs = List.map (fn (name, (flag,src,anf,cps)) => src) env; value
/seL4-l4v-master/HOL4/src/datatype/
H A DEnumType.sml248 val defs = map (new_definition o def) nclist value
[all...]
/seL4-l4v-master/HOL4/src/IndDef/
H A DInductiveDefinition.sml590 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 DtemporalLib.sml385 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 Dlisp_extractLib.sml549 val defs = map define_parts (zip data rs) value
/seL4-l4v-master/HOL4/src/metis/
H A DnormalForms.sml736 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 Dlisp_parseScript.sml2375 val defs = map mk_func tts value
2390 val defs = map mk_func2 tts value
/seL4-l4v-master/HOL4/examples/bootstrap/
H A DautomationLib.sml426 val defs = def |> CONJUNCTS |> map SPEC_ALL value
439 val defs = preprocess_def def value

Completed in 160 milliseconds

12