/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/ |
H A D | milawa_execScript.sml | 44 (!a fns s1 s2 t ts ok ok2. 46 MR_ev (Or ts,a,ctxt,fns,ok1) (s2,ok2) ==> 47 MR_ev (Or (t::ts),a,ctxt,fns,ok) (s2,ok2)) 49 (!e1 e2 e3 s1 s a ok1 ok2. 51 MR_ev (e3,a,ctxt,fns,ok1) (s,ok2) 53 MR_ev (If e1 e2 e3,a,ctxt,fns,ok) (s,ok2)) 55 (!e1 e2 e3 s1 s a ok1 ok2. 57 MR_ev (e2,a,ctxt,fns,ok1) (s,ok2) 59 MR_ev (If e1 e2 e3,a,ctxt,fns,ok) (s,ok2)) 61 (!e xs ys fns a ok1 ok2 [all...] |
H A D | milawa_initScript.sml | 27 (!xs fns io exp s fns2 io2 ok2 io3 ok3. 28 R_ev (sexp2term exp,FEMPTY,fns,io,T) (s,fns2,io2,ok2) /\ 30 R_aux_exec (exp::xs,fns,io) (io3,ok2 /\ ok3))`; 49 ``R_ev (sexp2term x1,FEMPTY,fns1,io1,T) (ans1,fns2,io2',ok2) /\ 61 R_aux_exec ([x1;x2;x3;x4;x5;x6],fns1,io1) (io7,ok2 /\ ok3 /\ ok4 /\ ok5 /\ ok6 /\ ok7)``, 65 \\ Q.LIST_EXISTS_TAC [`ans1`,`fns2`,`io2'`,`ok2`]
|
H A D | milawa_proofpScript.sml | 2519 !x1 x2 x3 x4 io ok. ?res ok2 io2. 2520 R_ap (Fun name,[x1;x2;x3;x4],ARB,k,io,ok) (res,k,io ++ io2,ok2) /\ 2521 (ok2 ==> (io2 = "")) /\ 2527 (x3 = list2sexp (MAP f2sexp thms)) /\ (x4 = atbl) /\ ok2 ==> 2606 let (res,k2,io2,ok2) = y in 2608 R_ap (f,args,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2)) /\ 2611 let (res,k2,io2,ok2) = y in 2613 R_evl (e,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2)) /\ 2616 let (res,k2,io2,ok2) = y in 2618 R_ev (e,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2))``, [all...] |
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
H A D | lisp_alt_semanticsScript.sml | 38 RR_ev (Or ts,a,fns1,io1,ok1) (s2,fns2,io2,ok2) ==> 39 RR_ev (Or (t::ts),a,fns,io,ok) (s2,fns2,io2,ok2)) 43 RR_ev (e3,a,fns1,io1,ok1) (s,fns2,io2,ok2) 45 RR_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2)) 49 RR_ev (e2,a,fns1,io1,ok1) (s,fns2,io2,ok2) 51 RR_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2)) 55 RR_ev (e,FUNION (VarBind xs sl) a,fns1,io1,ok1) (x,fns2,io2,ok2) 57 RR_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2)) 60 RR_evl (el,a,fns,io,ok) (args,fns1,io1,ok1) /\ RR_ap (fc,args,a,fns1,io1,ok1) (x,fns2,io2,ok2) /\ 63 RR_ev (App fc el,a,fns,io,ok) (x,fns2,io2,ok2)) [all...] |
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/spec/ |
H A D | lisp_semanticsScript.sml | 184 (!a fns io s1 fns1 io1 s2 fns2 io2 t ts ok ok2. 186 R_ev (Or ts,a,fns1,io1,ok1) (s2,fns2,io2,ok2) ==> 187 R_ev (Or (t::ts),a,fns,io,ok) (s2,fns2,io2,ok2)) 189 (!e1 e2 e3 s1 s a ok1 ok2. 191 R_ev (e3,a,fns1,io1,ok1) (s,fns2,io2,ok2) 193 R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2)) 195 (!e1 e2 e3 s1 s a ok1 ok2. 197 R_ev (e2,a,fns1,io1,ok1) (s,fns2,io2,ok2) 199 R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2)) 201 (!e xs ys fns a ok1 ok2 [all...] |
/seL4-l4v-master/HOL4/examples/Crypto/IDEA/ |
H A D | ideaScript.sml | 103 `InverseKeys (ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9) = 105 InverseKey ok5,InverseKey ok4,InverseKey ok3,InverseKey ok2, 216 ((ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9): OddKeySched) = 217 ListToOddKeys t ((k1,k2,k3,k4),ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8)) /\ 219 ((ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8,ok9): OddKeySched) = 220 ListToOddKeys t ((k1,k2,k3,k4),ok1,ok2,ok3,ok4,ok5,ok6,ok7,ok8))`;
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/minisat/ |
H A D | Main.C | 111 bool ok1 = false, ok2 = false; local 127 ok2 = true; 131 if (!ok1 || !ok2)
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/implementation/ |
H A D | lisp_correctnessScript.sml | 37 (!input fns io ok input2 exp rest s fns2 io2 io3 ok2 ok3. 40 R_ev (sexp2term exp,FEMPTY,fns,io,ok) (s,fns2,io2,ok2) /\ 41 R_exec (rest,fns2,io2 ++ sexp2string s ++ "\n",ok2) (io3,ok3) ==> 229 !input fns output output2 ok2. (x = (input,fns,output)) /\ (y = (output2,ok2)) ==> 237 (zERROR_MESSAGE ex \/ ~zS * zPC ^pc * zLISP_OUTPUT (IO_STREAMS "" output2,ok2))``, 262 BC_REFINES (fns2,io2) bc8 /\ bc_inv bc8 /\ (ok2 <=> bc8.ok)` by 293 |> (fn th => SPEC_BOOL_FRAME_RULE th ``R_exec (input,fns,"") (output2,ok2)``) 305 \\ REVERSE (Cases_on `ok2`) THEN1 310 |> Q.GEN `output2` |> Q.GEN `ok2` |> [all...] |
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_extractScript.sml | 52 ``(by ==> R_ev (y,e,fns1,io1,ok1) (ans2,fns2,io2,ok2)) /\ 60 if isTrue ans1 then ok2 else ok3)``, 126 ``R_evl (el,a,fns1,io1,ok1) (sl,fns2,io2,ok2) ==> 128 R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2)``, 133 ``(bl ==> R_evl (el,a,fns1,io1,ok1) (sl,fns2,io2,ok2)) ==> 135 (b /\ bl ==> R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2))``, 358 (b2 ==> R_ev (e,FUNION (VarBind xs sl) a,fns1,io1,ok1) (x,fns2,io2,ok2)) ==> 360 R_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2)``, 366 (b2 ==> R_ev (e,FUNION (VarBind xs sl) a,fns1,io1,ok1) (x,fns2,io2,ok2)) ==> 368 R_ev (Let (ZIP (xs,ys)) e,a,fns,io,ok) (x,fns2,io2,ok2)``, [all...] |
H A D | lisp_extractLib.sml | 402 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)`` 469 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)`` 912 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)``
|
/seL4-l4v-master/HOL4/src/HolSat/sat_solvers/zc2hs/ |
H A D | zc2hs.cpp | 113 bool ok1 = false, ok2 = false; local 129 ok2 = true; 133 if (!ok1 || !ok2)
|
/seL4-l4v-master/HOL4/src/update/ |
H A D | updateLib.sml | 285 val ok2 = Lib.can (Type.match_type (ty --> ty)) value 291 val _ = c_form orelse ok2 tm_ty andalso is_o_expr tm
|
/seL4-l4v-master/isabelle/src/Doc/Tutorial/document/ |
H A D | rules.tex | 2416 \ 2.\ ok2\isanewline 2425 \ 3.\ ok2
|
/seL4-l4v-master/l4v/isabelle/src/Doc/Tutorial/document/ |
H A D | rules.tex | 2416 \ 2.\ ok2\isanewline 2425 \ 3.\ ok2
|