/seL4-l4v-master/HOL4/examples/theorem-prover/milawa-prover/ |
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) /\ 2533 \\ Q.EXISTS_TAC `logic_proofp x1 x2 x3 x4` \\ Q.EXISTS_TAC `ok` 2605 let (f,args,env,k,io,ok) = x in 2608 R_ap (f,args,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2)) /\ 2610 let (e,env,k,io,ok) = x in 2613 R_evl (e,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2)) /\ 2615 let (e,env,k,io,ok) = x in 2618 R_ev (e,env,add_def k d,io,ok) (res,add_def k2 d,io2,ok2))``, 2632 ``R_ap (f,args,env,k,io,ok) (re [all...] |
/seL4-l4v-master/HOL4/examples/formal-languages/regular/regular-play/src/ |
H A D | regexSemanticsScript.sml | 65 (* ok, but not quite all - just 2 *)
|
/seL4-l4v-master/HOL4/examples/formal-languages/context-free/ |
H A D | grammarLib.sml | 13 fun ok e = return () e function 43 fun repeat (m : 'a tt) s = ((m >> repeat m) ++ ok) s 151 fun dropP P = repeat (getc "" >- (fn c => if P c then ok 161 if i = sz then ok 178 | Error _ => ok s 209 fun lex m = repeat ((getP Char.isSpace >> ok) ++ comment) >> m 210 fun complete m = m <- repeat ((getP Char.isSpace >> ok) ++ comment)
|
/seL4-l4v-master/HOL4/src/portableML/poly/concurrent/ |
H A D | Future.sml | 193 val ok = value 196 foldl' (fn job => fn ok => job valid andalso ok) jobs true) ()); 207 if ok andalso not (Exn.is_interrupt_exn test) then () 382 val ok = value 387 in ok end; 395 fun job ok = 398 if ok then 598 fun job ok = 599 assign_result group result (if ok the [all...] |
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | Cache.sml | 45 fun ok (prev,SOME thm) = prev << curr function 46 | ok (prev,NONE) = curr << prev 48 (case snd (first ok prevs) of 223 fun ok (cached, SOME _) = cached << hyps function 224 | ok (cached, NONE) = hyps << cached 226 case List.find ok cache_F of
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | qbuf.sml | 132 val (buffered, ok) = 140 if ok then
|
H A D | Pretype.sml | 73 UVar j => if i = j then ok 85 if v1 = v2 then ok 98 and unifyl [] [] = ok
|
/seL4-l4v-master/isabelle/src/Pure/General/ |
H A D | completion.scala | 434 val ok = 437 if (ok) Some((abbr, abbrevs)) 464 ok = 467 if ok
|
/seL4-l4v-master/l4v/isabelle/src/Pure/General/ |
H A D | completion.scala | 434 val ok = 437 if (ok) Some((abbr, abbrevs)) 464 ok = 467 if ok
|
/seL4-l4v-master/isabelle/src/Tools/VSCode/src/ |
H A D | server.scala | 276 if (!build(no_build = true).ok) { 283 if (!build().ok) { progress.echo(fail_msg); error(fail_msg) } 314 case Session.Terminated(result) if !result.ok => 345 if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/VSCode/src/ |
H A D | server.scala | 276 if (!build(no_build = true).ok) { 283 if (!build().ok) { progress.echo(fail_msg); error(fail_msg) } 314 case Session.Terminated(result) if !result.ok => 345 if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc)
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm/model/ |
H A D | armAssemblerLib.sml | 50 fun ok r = (Portable.inc pc; mlibUseful.INR r) function 73 then ok w :: p1 77 ( addWarning s1; ok w :: p1 )) 86 | WORD w => ok w :: p1
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/m0/model/ |
H A D | m0AssemblerLib.sml | 51 fun ok e r = (incpc e; mlibUseful.INR r) function 80 Thumb16 w => ok Enc_Narrow w :: p1 82 ok Enc_Wide (BitsN.@@ (w1, w2)) :: p1 95 | HALFWORD w => ok Enc_Narrow w :: p1
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
H A D | lisp_compilerScript.sml | 33 ok : bool |>`; 81 BC_FAIL bc = bc with ok := F`; 675 ~bc.ok ==> 715 ``(BC_ADD_CONST bc s).ok = bc.ok``, 725 (bc2.ok = bc.ok) /\ 733 (bc2.ok = bc.ok) /\ 741 (bc2.ok [all...] |
/seL4-l4v-master/isabelle/src/Tools/jEdit/src/ |
H A D | pretty_text_area.scala | 211 val (pattern, ok) = 223 if (ok) search_field_foreground
|
/seL4-l4v-master/l4v/isabelle/src/Tools/jEdit/src/ |
H A D | pretty_text_area.scala | 211 val (pattern, ok) = 223 if (ok) search_field_foreground
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/arm8/model/ |
H A D | arm8AssemblerLib.sml | 75 fun ok r = (Portable.inc pc; mlibUseful.INR r) function 97 then ok w :: p1 102 | WORD w => ok w :: p1
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64AssemblerLib.sml | 40 fun ok l = (incpc (List.length l); mlibUseful.INR l) function 58 | l => ok l :: p1) 64 | STREAM l => ok l :: p1
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | subtypeTools.sml | 208 val (ok,eq) = cmp (a,b) value 210 (if ok then ALL_CONV else comm_conv solver) THENC 215 val (ok,eq) = cmp (a,b) value 217 (if ok then ALL_CONV else comm_conv' solver) THENC 219 (if ok then ALL_CONV else push_conv' solver))
|
/seL4-l4v-master/HOL4/tools/Holmake/ |
H A D | Holmake_types.sml | 133 val (ok, spaces) = splitr Char.isSpace ss value 134 val (ok0, bslashes) = splitr (fn c => c = #"\\") ok 136 if size bslashes mod 2 = 0 then ok 138 slice(ss, 0, SOME (size ok + 1)) 139 else ok
|
H A D | internal_functions.sml | 59 val (ok, rest) = position (string from) ss value 62 recurse (to::ok::acc) (slice(rest, size from, NONE)) 63 else concat (List.rev (ok::acc))
|
/seL4-l4v-master/HOL4/examples/theorem-prover/lisp-runtime/extract/ |
H A D | lisp_extractLib.sml | 397 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``) 402 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)`` 461 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``) 469 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)`` 731 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v (args,fns,io,ok))``) 732 |> DISCH ``^v2 (args,fns,io,ok)`` |> PURE_REWRITE_RULE [AND_IMP_INTRO] 738 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) re [all...] |
/seL4-l4v-master/isabelle/src/Pure/Tools/ |
H A D | phabricator.scala | 165 if (!result.ok) error("Return code: " + result.rc.toString) 279 if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) { 314 if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) { 897 def ok: Boolean = error.isEmpty 898 def get: JSON.T = if (ok) result else Exn.error(error.get)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Tools/ |
H A D | phabricator.scala | 165 if (!result.ok) error("Return code: " + result.rc.toString) 279 if (!Isabelle_System.bash("mkdir -p " + File.bash_path(root_path)).ok) { 314 if (!Isabelle_System.bash("mkdir -p " + File.bash_path(repo_path)).ok) { 897 def ok: Boolean = error.isEmpty 898 def get: JSON.T = if (ok) result else Exn.error(error.get)
|
/seL4-l4v-master/HOL4/tools/Holmake/poly/ |
H A D | BuildCommand.sml | 339 (* incinfos not consulted for comparison so empty value ok here *) 444 fun interpret_graph (g,ok) = 445 (if ok then OS.Process.success else OS.Process.failure, g)
|