/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | preARMScript.sml | 178 read (regs,mem) (exp:EXP) = 179 case exp of 202 write (regs,mem) (exp:EXP) (v:DATA)= 203 case exp of
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | preARMScript.sml | 174 read (regs,mem) (exp:EXP) = 175 case exp of 197 write (regs,mem) (exp:EXP) (v:DATA)= 198 case exp of
|
/seL4-l4v-master/HOL4/examples/acl2/ml/ |
H A D | tutorial.ml | 39 [(``($**):num -> num -> num``,"exp")] 44 (* |- exp m arg = *) 55 (* val propagation_exp = |- nat (m ** arg) = exp (nat m) (nat arg) : thm *)
|
H A D | testACL2encoding.ml | 217 translate_simple_function [(``($**):num -> num -> num``,"exp")],
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Model.sml | 363 and expName = Name.fromString "exp" 399 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz)); 486 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Model.sml | 363 and expName = Name.fromString "exp" 399 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz)); 486 fun expFn sz x y = SOME (exp (multN sz) x y (oneN sz));
|
/seL4-l4v-master/HOL4/examples/algebra/monoid/ |
H A D | monoidOrderScript.sml | 128 ((Invertibles g).exp = $** ) 1025 ((Invertibles g).exp = g.exp)``,
|
/seL4-l4v-master/HOL4/examples/algebra/finitefield/ |
H A D | ffPolyScript.sml | 102 pfexp = (PolyRing (PF r)).prod.exp 1592 val _ = overload_on("pfexp", ``(PolyRing (PF r)).prod.exp``); 1602 ((PF r).prod.exp = $** ): thm 2545 and (PF r).prod.exp = $** by PF_property 2557 and (PF r).prod.exp = $** by PF_property 2770 Hence s.exp x (CARD B) = x by finite_field_fermat_thm 2781 Hence s.exp x (CARD B ** n) = x by finite_field_fermat_all
|
H A D | ffMasterScript.sml | 410 <=> s.prod.exp x n = x by poly_master_root 586 = (PolyModRing r p).prod.exp (X % p) (CARD (PolyModRing r p).carrier) by finite_field_fermat_thm 600 `X % p = (PolyModRing r p).prod.exp (X % p) (CARD (PolyModRing r p).carrier)` by rw[finite_field_fermat_thm] >> 618 <=> (PolyModRing r p).prod.exp x n = x by poly_master_root 619 <=> (PolyModRing r p).prod.exp (x % p) n = (x % p) by above 632 `!n. (PolyModRing r p).prod.exp (x % p) n = (x ** n) % p` by rw[poly_mod_field_exp] >> 3207 Thus g.exp x n IN G by group_exp_element 3208 g.exp x n 3209 = f*.exp x n by subgroup_exp
|
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyFieldModuloScript.sml | 4162 case OLEAST k. 0 < k /\ (((PolyModRing r z).prod excluding |0|).exp p k = |1|) of ... = 4163 case OLEAST k. 0 < k /\ (((PolyModRing r z).prod excluding |0|).exp (p % z) k = |1| of ... 4166 !k. ((PolyModRing r z).prod excluding |0|).exp p k = (p ** k) % z by poly_mod_exp_alt 4167 !k. ((PolyModRing r z).prod excluding |0|).exp (p % z) k = ((p % z) ** k) % z by poly_mod_exp_alt 4191 Hence ((PolyModRing r z).prod excluding |0|).exp (p % z) k 4212 `((PolyModRing r z).prod excluding |0|).exp (p % z) k = ((p % z) ** k) % z` by rw[poly_mod_exp_alt] >> 4310 Therefore !n. ((PolyModRing r z).prod excluding |0|).exp X n = (X ** n) % z by poly_mod_exp_alt 4312 Thus ((PolyModRing r z).prod excluding |0|).exp X m 4313 = ((PolyModRing r z).prod excluding |0|).exp X n by above 4336 `!n. ((PolyModRing r z).prod excluding |0|).exp [all...] |
H A D | polyMonicScript.sml | 59 ### = (poly_ring r).sum.exp |1| 60 |n| = (poly_ring r).sum.exp |1| n = ###n 61 |c| = (poly_ring r).sum.exp |1| c = ###c 682 val _ = overload_on ("##", ``r.sum.exp #1``); 683 val _ = overload_on ("###", ``(poly_ring r).sum.exp |1|``); 719 = (PolyRing r).sum.exp |1| 0 by notation
|
/seL4-l4v-master/graph-refine/ |
H A D | logic.py | 1565 def inst_eq_at_visit (exp, vis): 1566 if not exp.is_op ('EqSelectiveWrapper'): 1568 [_, xs, ys] = exp.vals
|
H A D | rep_graph.py | 222 for (exp, visit) in self.vals: 223 exp.serialise (ss)
|
/seL4-l4v-master/HOL4/src/quotient/examples/ |
H A D | more_setScript.sml | 38 (* For errors try <exp> handle e => Raise e;
|
/seL4-l4v-master/HOL4/examples/AI_tasks/ |
H A D | mleDiophSynt.sml | 487 writel "dioph_graph" ("gen exp sol" :: map graph_to_string graph);
|
H A D | mleCombinSynt.sml | 525 writel "combin_graph" ("gen exp sol" :: map graph_to_string graph);
|
/seL4-l4v-master/HOL4/src/AI/proof_search/ |
H A D | psMCTS.sml | 142 (Math.pow (x, alpha - 1.0) * Math.exp (~ x)) / gamma_of alpha
|
/seL4-l4v-master/HOL4/examples/machine-code/lisp/ |
H A D | lisp_finalScript.sml | 514 val th = SPEC_BOOL_FRAME_RULE th ``R_ev (s,FEMPTY) s2 /\ (exp = term2sexp s)`` 519 lisp_eval (exp,Sym "nil",Sym "nil",Sym "nil",Sym "nil",Sym "nil",l) =
|
/seL4-l4v-master/HOL4/examples/PSL/regexp/ |
H A D | matcherScript.sml | 1186 ``!exp : 'a regexp. ?dfa : (num->bool,'a) da. sem exp = da_accepts dfa``,
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | automationLib.sml | 131 (���:exp���,���exp���),
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | selftest.sml | 638 fun ptpp msg exp t = tpp msg exp lfcop_g t
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | heapsizing.cpp | 560 pagingCost = PAGINGCOSTFACTOR * exp(factor);
|
/seL4-l4v-master/HOL4/polyml/ |
H A D | configure | 9248 $ECHO "$_lt_compiler_boilerplate" | $SED '/^$/d' >conftest.exp 9250 if test ! -s conftest.er2 || diff conftest.exp conftest.er2 >/dev/null; then 9396 lt_prog_compiler_static='-bnso -bI:/lib/syscalls.exp' 9656 $ECHO "$_lt_compiler_boilerplate" | $SED '/^$/d' >conftest.exp 9658 if test ! -s conftest.er2 || diff conftest.exp conftest.er2 >/dev/null; then 9709 $ECHO "$_lt_linker_boilerplate" | $SED '/^$/d' > conftest.exp 9711 if diff conftest.exp conftest.er2 >/dev/null; then 9767 $ECHO "$_lt_compiler_boilerplate" | $SED '/^$/d' > out/conftest.exp 9769 if test ! -s out/conftest.er2 || diff out/conftest.exp out/conftest.er2 >/dev/null; then 9822 $ECHO "$_lt_compiler_boilerplate" | $SED '/^$/d' > out/conftest.exp [all...] |
/seL4-l4v-master/HOL4/examples/fermat/little/ |
H A D | FLTactionScript.sml | 74 Zadd_exp |- !n. 0 < n ==> !x m. (Zadd n).exp x m = (x * m) MOD n 193 (* |- !n. 0 < n ==> !x m. (Zadd n).exp x m = (x * m) MOD n *)
|
/seL4-l4v-master/HOL4/src/probability/ |
H A D | extrealScript.sml | 313 `(extreal_exp (Normal x) = Normal (exp x)) /\ 342 val _ = overload_on ("exp", Term `extreal_exp`); 2461 !x :extreal. 0 <= exp x 2475 !r. exp (Normal r) = Normal (exp r) 2489 exp 0 = (1 :extreal) 2542 ("EXP_LE_X_FULL", ``!x :real. &1 + x <= exp x``, 2552 >> Q.ABBREV_TAC `f = \x :real. exp x - (1 + x)` 2553 >> `exp x - (1 + x) = f x` by METIS_TAC [] >> POP_ORW 2554 >> Q.ABBREV_TAC `g = \x :real. exp [all...] |