/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/ |
H A D | github115aScript.sml | 5 val v1 = mk_var("v", bool --> bool) 6 val v2 = mk_var("v", bool)
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/tests/multibuild/ |
H A D | multiLib.sml | 7 val v = mk_var("v" ^ Int.toString n, bool)
|
/seL4-l4v-10.1.1/HOL4/src/refute/ |
H A D | selftest.sml | 3 fun Va n = mk_var("va" ^ Int.toString n, bool) 4 fun Vb n = mk_var("vb" ^ Int.toString n, bool)
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | inst_logic.py | 17 from syntax import mk_var namespace 96 inp_eqs = [((mk_var (nm, typ), 'ASM_IN'), (mk_var (nm, typ), 'C_IN')) 98 inp_eqs += [((logic.mk_rodata (mk_var (nm, typ)), 'ASM_IN'), 100 out_eqs = [((mk_var (nm, typ), 'ASM_OUT'), (mk_var (nm, typ), 'C_OUT')) 102 out_eqs += [((logic.mk_rodata (mk_var (nm, typ)), 'ASM_OUT'), 140 [syntax.mk_var (reg, syntax.word32T) for reg in inp_regs] 142 + [syntax.mk_var (nm, typ) for (nm, typ) in bin_globs],
|
/seL4-l4v-10.1.1/HOL4/src/1/ |
H A D | newtypeTools.sml | 23 val x = mk_var("x", oldty) and y = mk_var("y", oldty) 37 val g = mk_var("g", newty) and h = mk_var("h", newty)
|
H A D | Psyntax.sml | 8 val mk_var = Term.mk_var value
|
H A D | BoundedRewrites.sml | 13 ADD_ASSUM (mk_comb(bounded_tm, mk_var(Int.toString n, bool))) th
|
/seL4-l4v-10.1.1/HOL4/src/boss/ |
H A D | bool_defsScript.sml | 5 val LET_def = new_definition("LET_def",mk_eq(mk_var("LET",type_of(lhs(concl LET_DEF))),rhs(concl LET_DEF))) 7 val literal_case_def = new_definition("literal_case_def",mk_eq(mk_var("literal_case",type_of(lhs(concl literal_case_DEF))),rhs(concl literal_case_DEF))) 9 val IN_def = new_definition("IN_def",mk_eq(mk_var("IN",type_of(lhs(concl IN_DEF))),rhs(concl IN_DEF))) 11 val TYPE_DEFINITION_def = new_definition("TYPE_DEFINITION_def",mk_eq(mk_var("TYPE_DEFINITION",type_of(lhs(concl TYPE_DEFINITION))),rhs(concl TYPE_DEFINITION)))
|
/seL4-l4v-10.1.1/HOL4/src/floating-point/ |
H A D | machine_ieeeLib.sml | 36 val mode = Term.mk_var ("mode", rounding_ty) 51 val fp_to_float_var = Term.mk_var (fp_to_float, fp_ty --> float_ty) 52 val w = Term.mk_var ("w", fp_ty) 70 val float_to_fp_var = Term.mk_var (float_to_fp, float_ty --> fp_ty) 71 val x = Term.mk_var ("x", float_ty) 82 val fp_to_real_var = Term.mk_var (fp_to_real, fp_ty --> real_ty) 92 val fp_to_value_var = Term.mk_var (fp_to_value, fp_ty --> value_ty) 103 Term.mk_var (real_to_fp, rounding_ty --> real_ty --> fp_ty) 114 Term.mk_var 126 val a = Term.mk_var (" [all...] |
/seL4-l4v-10.1.1/HOL4/src/marker/ |
H A D | markerSyntax.sml | 19 let val l = mk_var(s,type_of tm) 34 val v1 = mk_var(s1,type_of rhs1) 35 val v2 = mk_var(s2,type_of rhs2) 52 REFL(mk_var(fst(dest_var tm),mk_vartype "'abbrev")) 79 list_mk_comb(label_tm, [mk_var(s, label_ty), t]);
|
/seL4-l4v-10.1.1/HOL4/src/boss/ml_evaluation/ |
H A D | Lift.sml | 24 val list_mk_comb_var = mk_var("list_mk_comb", Type`:'term -> 'term`) 25 val cons_var = mk_var ("cons",Type`:'term -> 'term -> 'term`) 26 val nil_var = mk_var ("nil",Type`:'term`) 27 val comma_var = mk_var (",",Type`:'term -> 'term -> 'term`) 33 val argvs = map mk_var (zip (enum_list "v" (length argtys)) argtys) 43 in mk_var(cname,ty') 54 val flist = map mk_var (zip flistnames flist_types) 57 val lift_var = mk_var("lift",lift_type) 68 Pair (mk_var(Cname,termty))
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/decompiler/ |
H A D | arm_core_decompLib.sml | 14 val r15 = Term.mk_var ("r15", ``:word32``) 26 val vars = Term.mk_var ("cond", Type.bool) ::
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/ |
H A D | congToolsLib.sml | 37 val var = mk_var ("x", hol_type) 49 val var1 = mk_var ("x1", hol_type) 50 val var2 = mk_var ("x2", hol_type) 51 val var3 = mk_var ("x3", hol_type)
|
/seL4-l4v-10.1.1/HOL4/src/HolSat/ |
H A D | satCommonTools.sml | 24 val mk_var = Term.mk_var; value 48 val t = mk_var("t",bool)
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/ |
H A D | HexSolitaireScript.sml | 80 if n<10 then mk_var("v0"^(int_to_string n),bool) 81 else mk_var("v"^(int_to_string n),bool); 84 if n<10 then mk_var("v0"^(int_to_string n)^"'",bool) 85 else mk_var("v"^(int_to_string n)^"'",bool); 93 fun mk_bool_var s = mk_var(s,bool);
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/examples/ |
H A D | ltl2omega.sml | 46 | mpattern_int n = subst [mk_var ("X", ``:'a ltl``) |-> mpattern_int (n-1)] 49 fun mpattern n = subst [mk_var ("X", ``:'a ltl``) |-> mpattern_int n] 55 | bpattern n = subst [mk_var ("X", ``:'a ltl``) |-> bpattern (n-1)] 88 subst [mk_var ("X1", ``:'a ltl``) |-> x1_term, 89 mk_var ("X2", ``:'a ltl``) |-> x2_term] pattern 100 val term = subst [mk_var ("X1", ``:'a ltl``) |-> t1, 101 mk_var ("X2", ``:'a ltl``) |-> t2, 102 mk_var ("X3", ``:'a ltl``) |-> t3] pattern 106 val term = subst [mk_var ("m", ``:'a ltl``) |-> m, 107 mk_var (" [all...] |
/seL4-l4v-10.1.1/HOL4/src/patricia/ |
H A D | patriciaLib.sml | 274 val p = Term.mk_var ("p", numLib.num) 275 val m = Term.mk_var ("m", numLib.num) 276 val k = Term.mk_var ("k", numLib.num) 277 val j = Term.mk_var ("j", numLib.num) 295 val d = Term.mk_var ("d", tty) 296 val l = Term.mk_var ("l", ty) 297 val r = Term.mk_var ("r", ty) 384 val p = Term.mk_var ("p", numLib.num) 385 val m = Term.mk_var ("m", numLib.num) 386 val j = Term.mk_var (" [all...] |
/seL4-l4v-10.1.1/HOL4/src/proofman/tests/ |
H A D | selftest.sml | 31 val f = mk_var("f", alpha --> alpha) 32 val gg = mk_var("g", beta --> gamma --> alpha) 33 val g = mk_var("g", gamma --> alpha) 34 val x = mk_var("x", gamma) 35 val b = mk_var("b", beta) 100 val t = boolSyntax.list_mk_conj (map(fn s => mk_var(s,bool)) strings)
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/ |
H A D | temporal_deep_simplificationsLib.sml | 51 val resultTerm = subst [mk_var("x", type_of t) |-> t, 52 mk_var("y", type_of t) |-> l, 53 mk_var("z", type_of t) |-> new_r] resultTerm 83 val resultTerm = subst [mk_var("x", type_of t) |-> t, 84 mk_var("y", type_of t) |-> l, 85 mk_var("z", type_of t) |-> new_r] resultTerm
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/graph/ |
H A D | stack_introLib.sml | 19 val th = th |> INST [m |-> mk_var("stack" ,type_of m), 20 d |-> mk_var("dom_stack" ,type_of d)] 44 val r13 = mk_var("r13",``:word32``)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/arm/ |
H A D | prog_armLib.sml | 35 in (mk_comb(``aR``,tm),mk_var("r" ^ f tm,``:word32``)) end 36 else if tm = ``psrN:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrn",``:bool``)) 37 else if tm = ``psrZ:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrz",``:bool``)) 38 else if tm = ``psrC:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrc",``:bool``)) 39 else if tm = ``psrV:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrv",``:bool``)) 40 else if tm = ``psrQ:arm_bit`` then (mk_comb(``aS1``,tm),mk_var("psrq",``:bool``)) 42 (mk_comb(``aM1:word32 -> word8 -> arm_set -> bool``,tm),mk_var(name_of_tm tm,``:word8``)) 46 val r15 = mk_var("r15",``:word32``) 53 val cpsr_var = mk_var("cpsr",``:word32``) 74 val code = subst [mk_var(" [all...] |
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/ |
H A D | ibmLib.sml | 344 mk_var ("i0", num) |-> i0, 345 mk_var ("s0", num) |-> s0] i0_le_s0_term; 350 mk_var ("A", ``:num symbolic_semi_automaton``) |-> A, 351 mk_var ("i0", num) |-> i0, 352 mk_var ("s0", num) |-> s0] state_vars_term; 358 mk_var ("A", ``:num symbolic_semi_automaton``) |-> A, 359 mk_var ("s0", num) |-> s0] used_vars_term; 372 mk_var ("p", ``:num prop_logic``) |-> p, 373 mk_var ("s0", num) |-> s0] used_vars_term; 501 mk_var ("ps [all...] |
/seL4-l4v-10.1.1/HOL4/examples/countable/ |
H A D | countable_initScript.sml | 61 val x = mk_var("x",ty) 62 val y = mk_var("y",ty)
|
H A D | countableLib.sml | 24 let val vs = Redblackmap.foldl (fn (n,ty,ls) => mk_var(n,ty)::ls) [] d 36 val v' = mk_var (Lib.prime n, ty) 43 val helpers = map (fn a => mk_var("count_"^(dest_vartype a),a --> num)) args 46 mk_var(count_name_aux, 71 val hyps = map (mk_inj_rwt_tm []) (zip (map (fn a => mk_var(dest_vartype a, a)) args) helpers)
|
/seL4-l4v-10.1.1/HOL4/src/num/theories/ |
H A D | basicSize.sml | 22 val lift_bool_var = mk_var("boolSyntax.lift_bool",ty --> bool --> tm) 50 val lift_one_var = mk_var("oneSyntax.lift_one", ty --> oneSyntax.one_ty --> tm)
|