| /seL4-l4v-10.1.1/HOL4/examples/machine-code/x64_compiler/ |
| H A D | x64_compilerLib.sml | 93 val pre = if is_conj (concl th2) then (last o CONJUNCTS) th2 else TRUTH value
94 val pre = RW [IF_IF,WORD_TIMES2] pre value
120 val pre = RW [] (foldr (uncurry CONJ) TRUTH pres) value
|
| /seL4-l4v-10.1.1/HOL4/src/TeX/ |
| H A D | holindexData.sml | 348 val pre = String.substring (thm, 0, String.size thm - 1); value
|
| /seL4-l4v-10.1.1/HOL4/src/floating-point/ |
| H A D | fp-functor.sml | 24 fun pre s = fp ^ "_" ^ s function
|
| /seL4-l4v-10.1.1/HOL4/src/metis/ |
| H A D | mlibTermnet.sml | 132 fun pre NONE = (0,NONE) | pre (SOME (i,n)) = (i, SOME n); function
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/ |
| H A D | prog_ppcLib.sml | 66 val pre = list_mk_star (map fst pre_post) ``:ppc_set -> bool`` value
79 val pre = subst ss pre value
81 val pre = if pre_conds = [] then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds)) value
167 val (pre,post) = ppc_pre_post g value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/pgcl/src/ |
| H A D | wpTools.sml | 102 val (pre,wlp_post) = dest_leq goal value
|
| /seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
| H A D | lisp_initScript.sml | 71 val pre = new_definition("init_func_pre",mk_eq(lhs_pre,f_pre)) value
|
| /seL4-l4v-10.1.1/HOL4/Manual/Translations/IT/Description/ |
| H A D | misc.tex | |
| /seL4-l4v-10.1.1/HOL4/examples/acl2/ml/ |
| H A D | translateLib.sml | 109 let val (pre,post) = (I ## tl) (split_after n concls); value
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/ |
| H A D | funCall.sml | |
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/ |
| H A D | funCall.sml | |
| /seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/ |
| H A D | swsepLib.sml | 121 val pre = hd args; value
|
| /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
| H A D | quantHeuristicsLibParameters.sml | 89 val pre = rand (rator (concl gthm)) value
|
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
| H A D | prog_x86Lib.sml | 84 val pre = list_mk_star (map fst pre_post) ``:x86_set -> bool`` value
101 val pre = subst ss pre value
103 val pre = mk_star (pre,``xPC eip``) value
105 val pre = if pre_conds = [] then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds)) value
217 val (pre,pos value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/lisp/ |
| H A D | lisp_finalScript.sml | 241 val pre = ``aLISP1 (t1,l) * aR 1w r1 * aSTRING_SPACE r1 (LENGTH (sexp2string t1)) * value
302 val pre = ``pLISP1 (t1,l) * pR 1w r1 * pSTRING_SPACE r1 (LENGTH (sexp2string t1)) * value
346 val pre = ``xSTACK (esp-4w) [w] * xR EDI edi * xR ESP esp * xPC p`` value
367 val pre = ``xSTACK esp [w] * ~xR EDI * xR ESP esp * xPC p`` value
388 val pre = ``xSTACK esp [w] * ~xR EDI * xR ESP esp * xPC p`` value
464 val pre = ``xLISP1 (t1,l) * xSTRING_SPACE w (LENGTH (sexp2string t1)) * value
[all...] |
| /seL4-l4v-10.1.1/HOL4/Manual/Description/ |
| H A D | misc.tex | |
| /seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
| H A D | TermNet.sml | 164 fun pre NONE = (0,NONE) function
|
| /seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
| H A D | TermNet.sml | 164 fun pre NONE = (0,NONE) function
|
| /seL4-l4v-10.1.1/HOL4/examples/dev/sw/ |
| H A D | funCall.sml | |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/compiler/ |
| H A D | compilerLib.sml | 96 val pre = if is_conj (concl th2) then (last o CONJUNCTS) th2 else TRUTH value
97 val pre = RW [IF_IF,WORD_TIMES2] pre value
120 val pre = RW [] (foldr (uncurry CONJ) TRUTH pres) value
133 val pre = fetch "-" (name ^ "_pre_def") value
211 val pre = get_pre tm value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
| H A D | prog_x64Lib.sml | 106 val pre = list_mk_star (map fst pre_post) ``:x64_set -> bool`` value
123 val pre = subst ss pre value
125 val pre = mk_star (``zPC rip``,pre) value
127 val pre = if pre_conds = [] then pre else mk_cond_star(pre,mk_comb(``Abbrev``,list_mk_conj pre_conds)) value
425 val (pre,pos value
[all...] |
| H A D | prog_x64_extraScript.sml | 790 val pre = ``w2n r8 DIV 8 < LENGTH (stack:word64 list) /\ value
823 val pre = ``w2n r8 DIV 8 < LENGTH (stack:word64 list) /\ value
892 val pre = ``k < LENGTH (stack:word64 list) /\ k < 268435456`` value
933 val pre value
[all...] |
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | kernel.c | 989 void bdd_default_gbchandler(int pre, bddGbcStat *s) argument
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/ |
| H A D | core_decompilerLib.sml | 573 val pre = get_assert (hd b) value
|
| /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/prog/ |
| H A D | riscv_progLib.sml | 247 val pre = progSyntax.strip_star o temporal_stateSyntax.dest_pre' o Thm.concl value
|