/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
H A D | lisp_compilerScript.sml | 1018 !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 D | lzConv.sml | 1613 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 D | Useful.sml | 87 fun exp m = function
|
H A D | Normalize.sml | 38 fun add logX logY = logX + Math.ln (1.0 + Math.exp (logY - logX));
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sml | 87 fun exp m = function
|
H A D | Normalize.sml | 38 fun add logX logY = logX + Math.ln (1.0 + Math.exp (logY - logX));
|
/seL4-l4v-master/HOL4/examples/AKS/theories/ |
H A D | AKSmapsScript.sml | 1585 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 D | AKSintroScript.sml | 597 !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 D | DefnBase.sml | 514 (* build (patterns,exp) pairs that will be body of case expression *)
|
/seL4-l4v-master/HOL4/examples/dev/sw2/examples/ |
H A D | arm_compiler_demoScript.sml | 65 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 D | definitions.tex | 225 | 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 D | vars_as_resourceFunctor.sml | 291 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 D | countPolyScript.sml | 790 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 D | Conv.sml | 2250 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 D | computeBasicScript.sml | 1425 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 D | ffSplitScript.sml | 1220 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 D | ffInstancesScript.sml | 874 `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 D | ffExistScript.sml | 1872 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 D | for_compileScript.sml | 1060 THEN1 (* For eval of exp fails *)
|
/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_proofpScript.sml | 2745 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 D | compile.sml | 513 (* CompileExp exp *) 515 (* [REC assumption] |- <circuit> ===> DEV exp *)
|
/seL4-l4v-master/HOL4/polyml/ |
H A D | ltmain.sh | 4652 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 D | polyRingScript.sml | 398 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 D | codegen_proofsScript.sml | 923 code_in t.pc (c_pops (xs:exp list) (vs:num option list))
|
/seL4-l4v-master/HOL4/examples/separationLogic/src/holfoot/ |
H A D | holfootScript.sml | 856 (FEVERY (\(tag,exp). 857 (IS_SOME (exp stack)) /\ 858 (THE (exp stack) = (heap ' loc) tag)) L)))`;
|