/seL4-l4v-10.1.1/HOL4/Manual/Description/ |
H A D | QuantHeuristics.tex | 497 val x = mk_var (v_name ^ "_hd", v_ty); 498 val xs = mk_var (v_name ^ "_tl", v_list_ty);
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
H A D | QuantHeuristics.tex | 487 val x = mk_var (v_name ^ "_hd", v_ty); 488 val xs = mk_var (v_name ^ "_tl", v_list_ty);
|
H A D | system.tex | 298 \index{mk_var@\ml{mk\_var}|pin} 300 mk_var : (string * hol_type) -> term 469 (mk_var("x",numty), 473 mk_var("x", numty)), 559 (mk_var("x",bool), 560 mk_eq(mk_var("x",numty), 779 \index{mk_var@\ml{mk\_var}} 791 {\small\verb+mk_var("+}$var${\small\verb+",+}$\sigma${\small\verb+)+} \\ \hline
|
/seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Tutorial/ |
H A D | logic.tex | 118 La funzione \ml{mk_var} costruisce una variabile da una stringa e un tipo. 124 - val x = mk_var("x", ``:bool``) 125 and y = mk_var("y", ``:bool``) 126 and z = mk_var("z", ``:bool``);
|
/seL4-l4v-10.1.1/HOL4/Manual/Tutorial/ |
H A D | logic.tex | 118 The function \ml{mk_var} constructs a variable from a string and a type. 124 - val x = mk_var("x", ``:bool``) 125 and y = mk_var("y", ``:bool``) 126 and z = mk_var("z", ``:bool``);
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/arm6-verification/ |
H A D | armLib.sml | 56 val X = variant vlist (mk_var("x",type_of M)) 65 val X = variant vlist (mk_var("x",type_of M))
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v4/ |
H A D | armLib.sml | 43 val X = variant vlist (mk_var("x",type_of M)) 52 val X = variant vlist (mk_var("x",type_of M))
|
H A D | arm_emitScript.sml | 54 FAIL num2register ^(mk_var("30 < n",bool)) n`, 75 FAIL num2condition ^(mk_var("15 < n",bool)) n`,
|
H A D | instructionSyntax.sml | 36 | mk_register (VReg x) = mk_var (x, ``:word4``);
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/ |
H A D | arm_parserLib.sml | 408 fun cast_var ty v = mk_var (fst (dest_var v),ty); 825 next_token >>- return (mk_var (Substring.string s,ty)) 1089 mk_var (s,``:word4``)
|
H A D | arm_random_testingLib.sml | 633 fun reg tm = mk_var ("r" ^ Int.toString (uint_of_word tm), ``:word32``); 634 fun flag tm = mk_var (fst (dest_const tm), bool); 635 val arch = mk_var ("architecture",``:ARMarch``) 636 val cpsr = mk_var ("cpsr", ``:ARMpsr``) 637 val spsr = mk_var ("spsr", ``:ARMpsr``) 638 val GE = mk_var ("GE", ``:word4``) 639 val IT = mk_var ("IT", ``:word8``) 640 val teehbr = mk_var ("TEEHBR", ``:word32``) 641 val mode = mk_var ("mode", ``:word5``) 642 val mem = mk_var ("me [all...] |
H A D | arm_stepLib.sml | 1154 val the_state = mk_var ("state",``:arm_seq_monad$arm_state``)
|
H A D | selftest.sml | 66 fun flag tm = mk_var (fst (dest_const tm), bool); 67 fun spsr_flag tm = mk_var ("s" ^ fst (dest_const tm), bool); 95 val GE = mk_var ("GE", ``:word4``); 96 val spsrGE = mk_var ("spsrGE", ``:word4``); 98 val mode = mk_var ("mode", ``:word5``); 99 val spsrmode = mk_var ("spsrmode", ``:word5``); 101 fun reg i = mk_var ("r" ^ Int.toString i, ``:word32``); 120 val mem = mk_var ("mem", ``:word32 -> word8``);
|
/seL4-l4v-10.1.1/HOL4/examples/ARM/v7/eval/ |
H A D | arm_emitScript.sml | 33 FAIL bytes ^(mk_var("n not 1, 2 or 4",bool)) (w,n)`, 49 | _ => FAIL parallel_add_sub_op1 ^(mk_var("can't decode",bool)) w`, 62 | _ => FAIL parallel_add_sub_op2 ^(mk_var("can't decode",bool)) w`, 76 ^(mk_var("can't decode",bool)) w`,
|
H A D | arm_evalLib.sml | 441 fun reg n = mk_var ("r" ^ Int.toString n, ``:word32``) 442 fun psr n = mk_var ("r" ^ Int.toString n, ``:ARMpsr``) 496 (mk_var ("r" ^ Int.toString i, typ) |->
|
H A D | arm_evalScript.sml | 146 fun reg n = mk_var ("r" ^ Int.toString n, ``:word32``) 175 fun psr n = mk_var ("r" ^ Int.toString n, ``:ARMpsr``)
|
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/ |
H A D | ARM_proverLib.sml | 418 val gen_var = (mk_var("y", abs_type))
|
H A D | ARM_prover_extLib.sml | 262 val gen_var = (mk_var("y", abs_type))
|
H A D | user_lemma_primitive_operationsScript.sml | 468 THEN ASSUME_TAC (SPECL [``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``, ``s1:arm_state``, mk_var ("H", H_sig)] (GEN_ALL simp_ext_lem)) 469 THEN ASSUME_TAC (SPECL [``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``, ``s2:arm_state``, mk_var ("H", H_sig)] (GEN_ALL simp_ext_lem)) 470 THEN ASSUME_TAC (SPECL (List.concat [[``s1:arm_state``], additional_spec_list, [mk_var ("H", H_sig), ``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``]]) effect_fixed_lem) 471 THEN ASSUME_TAC (SPECL (List.concat [[``s2:arm_state``], additional_spec_list, [mk_var ("H", H_sig), ``xI:bool``, ``(s2.psrs (0,CPSR)).F:bool``]]) effect_fixed_lem)
|
/seL4-l4v-10.1.1/HOL4/examples/CCS/ |
H A D | CCSConv.sml | 152 val U = mk_var ("u", type_of (hd actl)); 302 val U = mk_var ("u", type_of (hd actl));
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
H A D | DerivedBddRules.sml | 215 else Psyntax.mk_cond(mk_var(get_node_name(bdd.var bdd),bool), 318 val ntm = mk_var("n",num) 692 SOME(s,_) => BddVar true vm (mk_var(s,bool)) 807 val prime_var = mk_var o (prime ## I) o dest_var 904 SOME(s,_) => mk_var(s,bool)
|
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/KatiPuzzle/ |
H A D | KatiPuzzleScript.sml | 76 (fn s => mk_var(s,bool)) 167 (mk_var("s",type_of s))
|
/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);
|
H A D | MiniTLHexSolitaireScript.sml | 63 if n<10 then mk_var("v0"^(int_to_string n),bool) 64 else mk_var("v"^(int_to_string n),bool); 71 if n<10 then mk_var("v0"^(int_to_string n)^"'",bool) 72 else mk_var("v"^(int_to_string n)^"'",bool); 95 (fn s => mk_var(s,bool)) 199 (mk_var("s",type_of s))
|
H A D | SolitaireScript.sml | 71 fun mk_bool_var s = mk_var(s,bool)
|