| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/step/ |
| H A D | arm_configLib.sig | 7 val st: term value
|
| H A D | arm_configLib.sml | 24 val st = Term.mk_var ("s", Type.mk_type ("arm_state", [])) value
|
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/Examples/Solitaire/ |
| H A D | SolitaireScript.sml | 89 val st = list_mk_pair (map mk_bool_var var_list) value
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | qbuf.sml | 69 val st = base_lexer.UserDeclarations.newstate nf value
|
| H A D | PPBackEnd.sml | 87 fun top_style style_stack = let val st = !style_stack in value
90 fun pop_style style_stack = let val st = !style_stack in value
[all...] |
| H A D | type_grammar.sml | 295 val st = type_to_structure ty value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
| H A D | bddTools.sml | 235 else let val st = strip_pair state value
|
| H A D | ctlTools.sml | 49 val (st,st') = (strip_pair##strip_pair) (state,state') value
|
| H A D | cearTools.sml | 118 val (st,ast) = (strip_pair ## strip_pair) (dest_pair(snd(dest_comb(getTerm abs_fun)))) value
245 val st = strip_pair state value
534 val (st,st') = (strip_pair state,strip_pair state') value
666 val st = pairSyntax.strip_pair state value
[all...] |
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | parse_glob.sml | 35 fun (st >- f) s = function
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/prog/ |
| H A D | x64_progLib.sml | 131 val st = Term.mk_var ("s", ``:x64_state``) value
|
| /seL4-l4v-10.1.1/HOL4/polyml/mlsource/MLCompiler/ |
| H A D | Pretty.sml | 244 val st = projPrettyString p value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/step/ |
| H A D | arm8_stepScript.sml | 439 val st = ``s: arm8_state`` value
|
| H A D | arm8_stepLib.sml | 95 val st = ``s: arm8_state`` value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/step/ |
| H A D | mips_stepScript.sml | 323 val st = ``s:mips_state`` value
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | TypeBase.sml | 226 val st = TYOP {Args = List.tabulate(i, PARAM), Thy = thy, Tyop = nm} value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/cheri/step/ |
| H A D | cheri_stepLib.sml | 363 val st = ``s:cheri_state`` value
[all...] |
| H A D | cheri_stepScript.sml | 209 val st = ``s:cheri_state`` value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/mips/prog/ |
| H A D | mips_progLib.sml | 35 val st = Term.mk_var ("s", ``:mips_state``) value
|
| /seL4-l4v-10.1.1/HOL4/src/num/ |
| H A D | numLib.sml | 171 val st = find_subterm qtm g value
200 val st = BasicProvers.prim_find_subterm FVs arg g value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | mechReasoning.sml | 222 val st = if is_imp t1 then rhs (#2 (dest_imp t1)) else rhs t1 value
248 val st = mk_pair (mk_var ("regs", Type `:REGISTER |-> DATA`), mk_var ("mem", Type `:ADDR |-> DATA`)); value
412 val st = mk_var ("st", Type `:DSTATE`); value
534 val st = mk_var ("st", Type `:DSTATE`); value
578 val st = mk_var ("st", Type `:DSTATE`); value
675 val st = mk_var ("st", Type `:DSTATE`); value
738 val st = mk_var ("st", Type `:DSTATE`); value
772 val st = mk_var ("st", Type `:DSTATE`); value
807 val st = mk_var ("st", Type `:DSTATE`); value
1021 let val st = mk_pair (mk_var ("regs", Type `:num |-> DATA`), mk_var ("mem", Type `:num |-> DATA`)); value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/prog/ |
| H A D | arm8_progLib.sml | 213 val st = Term.mk_var ("s", ``:arm8_state``) value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/prog/ |
| H A D | riscv_progLib.sml | 37 val st = Term.mk_var ("s", ``:riscv_state``) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_opsScript.sml | 871 val st = int_to_string (i+2) value
890 val st = int_to_string (i+2) value
911 val st = x86_reg i value
934 val st = x86_reg i value
960 val st = int_to_string (i+2) value
980 val st = int_to_string (i+2) value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/HolBdd/ |
| H A D | DerivedBddRules.sml | 311 val (st,st') = dest_pair st_st' value
|