/seL4-l4v-master/HOL4/examples/dev/sw/ |
H A D | annotatedIR.sml | 21 type annt = {fspec : thm, ins : exp, outs : exp, context : exp list}; 24 type cond = exp * rop * exp;
|
H A D | funCall.sml | 204 | one_arg (exp, (invRegLs, i)) = 205 (isBroken := true; (([exp],false, i) :: invRegLs, i-1)) 408 List.map (fn exp => ( i := !i + 1; MEM(11, ~(3 + (len - !i))))) expL
|
H A D | preARMScript.sml | 182 read (regs,mem) (exp:EXP) = 183 case exp of 206 write (regs,mem) (exp:EXP) (v:DATA)= 207 case exp of
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/ |
H A D | annotatedIR.sml | 12 type annt = {fspec : thm, ins : exp, outs : exp, context : exp list}; 15 type cond = exp * rop * exp;
|
H A D | funCall.sml | 192 | one_arg (exp, (invRegLs, i)) = 193 (isBroken := true; (([exp],false, i) :: invRegLs, i-1)) 396 List.map (fn exp => ( i := !i + 1; MEM(11, ~(3 + (len - !i))))) expL
|
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/ |
H A D | annotatedIR.sml | 12 type annt = {fspec : thm, ins : exp, outs : exp, context : exp list}; 15 type cond = exp * rop * exp;
|
H A D | funCall.sml | 189 | one_arg (exp, (invRegLs, i)) = 190 (isBroken := true; (([exp],false, i) :: invRegLs, i-1)) 393 List.map (fn exp => ( i := !i + 1; MEM(11, ~(3 + (len - !i))))) expL
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | selftest.sml | 872 val cl = LS[`exp $x 0 = 1`]; 874 val cl = LS[`$y = 0`,`exp $x $y = $x * exp $x (pre $y)`]; 1035 and expFnName = Name.fromString "exp" 1064 `$y <= exp $x`]);
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_extractScript.sml | 420 ``!fns2 io io2 args a fc fns params exp x ok2 res. 421 fc IN FDOM fns /\ (fns ' fc = (params,exp)) /\ 423 R_ev (exp,VarBind params args,fns,io,ok) res ==> 430 (b ==> R_ap (Fun name,args,e,k,io,ok) exp) ==> 433 ((ok ==> b) ==> R_ap (Fun name,args,e,k,io,ok) (if ok then exp else (Sym "NIL",k,io,ok)))``,
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | selftest.sml | 872 val cl = LS[`exp $x 0 = 1`]; 874 val cl = LS[`$y = 0`,`exp $x $y = $x * exp $x (pre $y)`]; 1035 and expFnName = Name.fromString "exp" 1064 `$y <= exp $x`]);
|
/seL4-l4v-master/HOL4/examples/algebra/polynomial/ |
H A D | polyBinomialScript.sml | 322 ((PolyRing r).prod.exp (x + y) 2 = 323 (PolyRing r).prod.exp x 2 + 324 (PolyRing r).sum.exp |1| 2 * (x * y) + 325 (PolyRing r).prod.exp y 2) : thm 332 ((PolyRing r).prod.exp (p + q) 2 = 333 (PolyRing r).prod.exp p 2 + 334 (PolyRing r).sum.exp |1| 2 * (p * q) + 335 (PolyRing r).prod.exp q 2) : thm 337 val _ = overload_on ("**", ``(PolyRing r).prod.exp``); 344 p ** 2 + (PolyRing r).sum.exp | [all...] |
/seL4-l4v-master/HOL4/src/tfl/src/ |
H A D | Defn.sml | 1592 fun exp (AQ(locn,tm)) S = function 1594 | exp (IDENT (p as (locn,s))) S = 1598 | exp (QIDENT (p as (locn,s,_))) S = 1600 then raise ERRloc "exp" locn "wildcard in long id. in pattern" 1602 | exp (APP(locn,M,N)) S = 1603 let val (M',S') = exp M S 1604 val (N', S'') = exp N S' 1607 | exp (TYPED(locn,M,pty)) S = 1608 let val (M',S') = exp M S in (TYPED(locn,M',pty),S') end 1609 | exp (LA [all...] |
/seL4-l4v-master/HOL4/src/probability/ |
H A D | derivativeScript.sml | 1894 ``!z. ((\n. z pow n / (&(FACT n))) sums exp(z)) (from 0)``, 1895 SIMP_TAC std_ss [exp] THEN 1909 ``!w z. ((\n. z pow n / (&(FACT n))) sums w) (from 0) <=> (w = exp(z))``, 1917 ==> abs(sum((0:num)..n) (\i. z pow i / (&(FACT i))) - exp(z)) <= e``, 1939 ``!z. (exp has_derivative (\y. exp z * y)) (at z)``, 1944 `exp:real->real`, `from (0)`] 1958 exp x) <= e) /\ 1994 MAP_EVERY Q.EXISTS_TAC [`(&0)`, `exp((&0))`] THEN 2034 ``!z. exp continuou [all...] |
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | fieldTools.sml | 641 val (exp,varmap) = field_to_exp tm [] value 657 val exp = Algebra.normalize {equations = eqns} exp value 659 val tm' = exp_to_field field varmap exp
|
/seL4-l4v-master/HOL4/src/integer/ |
H A D | OmegaMath.sml | 1087 relations of the form d | exp where exp includes at least one 1118 relations of the form ~(d | exp) where exp includes at least one
|
H A D | intSyntax.sml | 91 val dest_exp = dest_binop exp_tm ("dest_exp", "Term not an exp")
|
/seL4-l4v-master/HOL4/src/n-bit/ |
H A D | blastLib.sml | 244 mk_summation : returns theorems of the form ``BSUM i x y c = exp`` 245 for all 0 < i < max, where "exp" is a propositional 307 mk_carry : returns theorem of the form ``BCARRY max x y c = exp``, 308 where "exp" is a propositional expression.
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfoot_pp_print.sml | 675 (fn (tag,exp) => 678 sys (Top, Top, Top) (d - 1) exp 696 (fn (tag,exp) => 699 sys (Top, Top, Top) (d - 1) exp
|
/seL4-l4v-master/HOL4/examples/algebra/field/ |
H A D | fieldInstancesScript.sml | 500 ((GF n).sum.exp 1 n = 0) /\ 501 !m. 0 < m /\ m < n ==> (GF n).sum.exp 1 m <> 0 535 `((GF n).sum.exp 1 n = 0) /\ !m. 0 < m /\ m < n ==> (GF n).sum.exp 1 m <> 0` suffices_by metis_tac[finite_ring_char_alt] >>
|
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/ |
H A D | BaseCodeTreeSig.sml | 107 | Handle of (* Exception handler. *) { exp: codetree, handler: codetree, exPacketAddr: int }
|
H A D | BackendIntermediateCodeSig.sml | 75 | BICHandle of (* Exception handler. *) { exp: backendIC, handler: backendIC, exPacketAddr: int }
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | exporter.cpp | 576 ExportRequest(Handle root, Exporter *exp): MainThreadRequest(MTP_EXPORTING), argument 577 exportRoot(root), exporter(exp) {}
|
/seL4-l4v-master/HOL4/examples/algebra/finitefield/ |
H A D | ffConjugateScript.sml | 897 Hence order r.prod (f*.exp x (CARD B ** n)) * (gcd a (CARD B ** n)) = a by group_order_power 1467 ZN_exp |- !n. 0 < n ==> !x k. (ZN n).prod.exp x k = x ** k MOD n 1551 !n m. n < forder x /\ m < forder x /\ (f*.exp x n = f*.exp x m) ==> (n = m): 1554 !x. x IN g.carrier ==> !n m. n < order g x /\ m < order g x /\ ((g.exp x n = (g.exp x m) ==> (n = m): thm 1584 Note f*.exp = $** by field_nonzero_mult_property 1601 Note !x k. g.exp x k = (ZN ox).prod.exp x k by Invertibles_property 1602 and !x k. (ZN ox).prod.exp [all...] |
/seL4-l4v-master/HOL4/examples/dev/ |
H A D | compile.sig | 146 (* CompileExp exp *) 148 (* [REC assumption] |- <circuit> ===> DEV exp *)
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibModel.sml | 126 | func ("exp",[m,n]) = SOME (funpow n (fn x => f (x * m)) one) 156 | func ("exp",[m,n]) = SOME (funpow n (fn x => f (x * m)) one)
|