| /seL4-l4v-10.1.1/HOL4/src/integer/testing/ |
| H A D | genproblem.sml | 7 val vars = map (fn s => mk_var(s, num)) ["u", "v", "x", "y", "z"] value
|
| H A D | gen_bc_problem.sml | 7 val vars = map (fn s => mk_var(s, int_ty)) ["u", "v", "x", "y", "z"] value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/decompiler/ |
| H A D | arm_core_decompLib.sml | 26 val vars = Term.mk_var ("cond", Type.bool) :: value
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibTermorder.sig | 28 val vars : termorder -> string list value
|
| H A D | folMapping.sig | 16 type vars = term list * hol_type list type
|
| H A D | folTools.sig | 21 type vars = term list * hol_type list type
|
| H A D | mlibTermorder.sml | 82 let val vars = vars @ [""] in fn eqn => map (M.count eqn) vars end; value
275 fun vars (TO (_,fvs,_,_)) = fvs; function
[all...] |
| /seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
| H A D | Instance.sml | 76 val vars = map (genvar o type_of) insts value
|
| H A D | Sol_ranges.sml | 176 val vars = vars_of_coeffs coeffsl value
|
| H A D | Sup_Inf.sml | 380 val vars = vars_of_coeffs set value
|
| /seL4-l4v-10.1.1/HOL4/examples/muddy/ |
| H A D | fdd.sig | 13 val vars: fddvar -> bdd.varnum list value
|
| H A D | fdd.sml | 33 val vars: fddvar -> bdd.varnum list = value
|
| /seL4-l4v-10.1.1/HOL4/src/pred_set/src/ |
| H A D | pred_setSimps.sml | 24 val (vars,body) = dest_pabs arg value
|
| /seL4-l4v-10.1.1/HOL4/src/simp/src/ |
| H A D | Satisfy.sml | 57 let val (vars,g) = strip_exists gl value
|
| /seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/ |
| H A D | ibm.sml | 284 val vars = fair_empty_ks2smv_string ks file_st; value
|
| /seL4-l4v-10.1.1/HOL4/src/taut/ |
| H A D | tautLib.sml | 48 let val (vars,tm') = strip_forall tm value
51 let val (vars,tm') = strip_forall tm value
110 let val vars = free_vars tm value
189 val vars value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/miller/ho_prover/ |
| H A D | skiTools.sig | 14 type vars = HurdUseful.vars type
|
| H A D | unifyTools.sig | 14 type vars = HurdUseful.vars type
|
| H A D | ho_basicTools.sig | 13 type vars = HurdUseful.vars type
|
| H A D | ho_discrimTools.sig | 13 type vars = HurdUseful.vars type
|
| /seL4-l4v-10.1.1/HOL4/src/new-datatype/ |
| H A D | Witness.sml | 39 val vars = map type_of ((fst o strip_forall o concl) thm) value
|
| /seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
| H A D | QbfLibrary.sml | 289 val (vars, hyp) = merge_vars (vars1, hyp1) (vars2, hyp2) value
|
| /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibParameters.sml | 62 val vars = map (fn (n, ty) => (mk_var (vn^"_"^(Int.toString n), ty))) ntL value
81 val vars = case (P v t) of NONE => raise QUANT_INSTANTIATE_HEURISTIC___no_guess_exp value
132 val vars = fst (pairSyntax.dest_pabs (fst (dest_comb p))) value
340 val vars = let value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/ |
| H A D | m1-story.lisp | [all...] |
| /seL4-l4v-10.1.1/HOL4/examples/ |
| H A D | dpll.sml | 153 val vars = map (fn t => genvar bool) insts value
|