Searched refs:exp (Results 201 - 225 of 228) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/
H A Dlisp_compilerScript.sml1018 !fc params exp.
1019 fc IN FDOM fns /\ (fns ' fc = (params,exp)) ==>
1023 BC_ev T (exp,MAP ssVAR (REVERSE params),p,bc4)
1576 ``BC_ev ret (exp,a,p,bc) (code,a2,p2,bc0) ==>
2143 \\ Q.PAT_X_ASSUM `!fc params.bbb` (MP_TAC o Q.SPECL [`fc`,`params`,`exp`])
2239 \\ Q.PAT_X_ASSUM `!fc params. bbb` (MP_TAC o Q.SPECL [`fc`,`params`,`exp`])
2640 \\ Q.PAT_X_ASSUM `!fc params.bbb` (MP_TAC o Q.SPECL [`fname`,`params`,`exp`])
/seL4-l4v-master/HOL4/examples/HolCheck/
H A DlzConv.sml1613 val exp = RIGHT_BETA(AP_THM def Rand) value
1616 SUBST [v |-> conv (Bvar,y) (rand(rand(concl exp)))]
1617 (mk_eq{lhs=tm, rhs=mk_conj{conj1=mk_exists ab, conj2=v}}) exp
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DUseful.sml87 fun exp m = function
H A DNormalize.sml38 fun add logX logY = logX + Math.ln (1.0 + Math.exp (logY - logX));
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DUseful.sml87 fun exp m = function
H A DNormalize.sml38 fun add logX logY = logX + Math.ln (1.0 + Math.exp (logY - logX));
/seL4-l4v-master/HOL4/examples/AKS/theories/
H A DAKSmapsScript.sml1585 Hence ((PolyModRing r z).prod excluding |0|).exp p k
1609 `((PolyModRing r z).prod excluding |0|).exp p k = (p ** k) % z` by rw[poly_mod_exp_alt] >>
1628 Hence ((PolyModRing r z).prod excluding |0|).exp (p % z) k
1654 `((PolyModRing r z).prod excluding |0|).exp (p % z) k = ((p % z) ** k) % z` by rw[poly_mod_exp_alt] >>
H A DAKSintroScript.sml597 !n. Poly (PolyModRing r z) ((PolyRing (PolyModRing r z)).prod.exp p n): thm
620 (((PolyModRing r z).prod.exp (poly_eval (PolyModRing r z) (lift p) X) n) =
/seL4-l4v-master/HOL4/src/coretypes/
H A DDefnBase.sml514 (* build (patterns,exp) pairs that will be body of case expression *)
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/
H A Darm_compiler_demoScript.sml65 p ::= let r = exp in p
74 exp ::= m | mode | ~ mode | r op mode | r * r
/seL4-l4v-master/HOL4/Manual/Translations/IT/Description/
H A Ddefinitions.tex225 | let_exp of dec => exp ;
227 exp = aexp of atexp
228 | app_exp of exp => atexp
234 rule = rule of pat => exp ;
240 valbind = bind of pat => exp
241 | bindl of pat => exp => valbind
/seL4-l4v-master/HOL4/examples/separationLogic/src/
H A Dvars_as_resourceFunctor.sml291 val exp = (intro_cond_hoare_triple thm; UNCHANGED) handle x => x
292 val exp =
295 val resource_and_proc_call_free_PROVE___failed_expn(_, tt, _) = exp
3333 al exp = (intro_hoare_triples current_theorem; UNCHANGED) handle x => x
3334 val resource_and_proc_call_free_PROVE___failed_expn(_, _, SOME tt) = exp
/seL4-l4v-master/HOL4/examples/AKS/machine/
H A DcountPolyScript.sml790 Let c = (ZN n).sum.exp (ZN n).prod.id 1.
807 qabbrev_tac `c = (ZN n).sum.exp (ZN n).prod.id 1` >>
1185 = PAD_RIGHT (ZN n).sum.id k [(ZN n).sum.exp (ZN n).prod.id c] by ZN_num_mod
1196 `_ = PAD_RIGHT (ZN n).sum.id k [(ZN n).sum.exp (ZN n).prod.id c]` by rw[ZN_num_mod, ZN_property] >>
1433 = [(ZN n).sum.exp (ZN n).prod.id 1] by ZN_num_1
/seL4-l4v-master/HOL4/src/1/
H A DConv.sml2250 val exp = RIGHT_BETA (AP_THM def Rand) value
2253 SUBST [v |-> conv (Bvar, y) (rand (rand (concl exp)))]
2255 rhs = mk_conj {conj1 = mk_exists ab, conj2 = v}}) exp
/seL4-l4v-master/HOL4/examples/AKS/compute/
H A DcomputeBasicScript.sml1425 if (exp b c = n) return (b, c)
1432 if (exp b c = n) return (b, c)
/seL4-l4v-master/HOL4/examples/algebra/finitefield/
H A DffSplitScript.sml1220 Let z = f*.exp y h
1256 qabbrev_tac `z = f*.exp y h` >>
2329 or ring_sub (PolyModRing r z) ((PolyModRing r z).prod.exp x n) |1| = |0| by poly_unity_eval
2330 or (PolyModRing r z).prod.exp x n = |1| by ring_sub_eq_zero
H A DffInstancesScript.sml874 `GF_4.sum.op x x = GF_4.prod.op (GF_4.sum.exp GF_4.prod.id 2) x` by rw_tac std_ss[field_single_add_single] >>
H A DffExistScript.sml1872 Consider the map: f = \x. s.prod.exp b (idx x).
1919 f x = if x = #0 then s.sum.id else s.prod.exp (primitive s) (idx x)
/seL4-l4v-master/HOL4/examples/fun-op-sem/for/
H A Dfor_compileScript.sml1060 THEN1 (* For eval of exp fails *)
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/
H A Dmilawa_proofpScript.sml2745 let (exp,env,k,io,ok) = x in
2748 R_evl (exp,env,k3,io,ok) (res,k3,io2,ok2)) /\
2750 let (exp,env,k,io,ok) = x in
2753 R_ev (exp,env,k3,io,ok) (res,k3,io2,ok2))``,
2840 (def_axiom name (params,WITNESS_FUN exp var_name,sem) =
2841 (Or (Equal exp (mConst (Sym "NIL")))
2842 (Not (Equal (mLamApp (var_name::params) exp
/seL4-l4v-master/HOL4/examples/dev/
H A Dcompile.sml513 (* CompileExp exp *)
515 (* [REC assumption] |- <circuit> ===> DEV exp *)
/seL4-l4v-master/HOL4/polyml/
H A Dltmain.sh4652 export_symbols=$output_objdir/$outputname.exp
4665 eval "$SED -e 's/\([].[*^$]\)/\\\\\1/g' -e 's/^/ /' -e 's/$/$/'"' < "$export_symbols" > "$output_objdir/$outputname.exp"'
4666 eval '$GREP -f "$output_objdir/$outputname.exp" < "$nlist" > "$nlist"T'
9660 export_symbols=$output_objdir/$libname.exp
9926 export_symbols=$output_objdir/$libname.exp
/seL4-l4v-master/HOL4/examples/algebra/polynomial/
H A DpolyRingScript.sml398 poly_one_sum_n |- !r. Ring r ==> !n. (PolyRing r).sum.exp |1| n = chop [##n]
4534 = (PolyRing r).sum.exp |1| n
4535 = (PolyRing r).sum.exp |0| n by poly_one, poly_zero
/seL4-l4v-master/HOL4/examples/bootstrap/
H A Dcodegen_proofsScript.sml923 code_in t.pc (c_pops (xs:exp list) (vs:num option list))
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/
H A DholfootScript.sml856 (FEVERY (\(tag,exp).
857 (IS_SOME (exp stack)) /\
858 (THE (exp stack) = (heap ' loc) tag)) L)))`;

Completed in 330 milliseconds

12345678910