Searched refs:ok (Results 51 - 75 of 130) sorted by relevance

123456

/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/src/
H A DregexSemanticsScript.sml65 (* ok, but not quite all - just 2 *)
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DgrammarLib.sml13 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-10.1.1/HOL4/src/portableML/poly/concurrent/
H A DFuture.sml193 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-10.1.1/HOL4/src/simp/src/
H A DCache.sml45 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-10.1.1/HOL4/src/parse/
H A DGrammarDeltas.sml131 val (ok,notok) = Lib.partition check_delta deltas value
140 set_theory_data {thydataty = tmtag, data = toData ok})
H A DPretype.sml73 UVar j => if i = j then ok
85 if v1 = v2 then ok
98 and unifyl [] [] = ok
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dcompletion.scala434 val ok =
437 if (ok) Some((abbr, abbrevs))
464 ok =
467 if ok
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dcompletion.scala434 val ok =
437 if (ok) Some((abbr, abbrevs))
464 ok =
467 if ok
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/
H A DarmAssemblerLib.sml50 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-10.1.1/HOL4/examples/l3-machine-code/m0/model/
H A Dm0AssemblerLib.sml51 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-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/bytecode/
H A Dlisp_compilerScript.sml32 ok : bool |>`;
80 BC_FAIL bc = bc with ok := F`;
674 ~bc.ok ==>
714 ``(BC_ADD_CONST bc s).ok = bc.ok``,
724 (bc2.ok = bc.ok) /\
732 (bc2.ok = bc.ok) /\
740 (bc2.ok
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/
H A Ddump.scala135 if (theories_result.ok) session_result
138 (name, status) <- theories_result.nodes if !status.ok
/seL4-l4v-10.1.1/isabelle/src/Tools/jEdit/src/
H A Dpretty_text_area.scala211 val (pattern, ok) =
223 if (ok) search_field_foreground
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/
H A Ddump.scala135 if (theories_result.ok) session_result
138 (name, status) <- theories_result.nodes if !status.ok
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/jEdit/src/
H A Dpretty_text_area.scala211 val (pattern, ok) =
223 if (ok) search_field_foreground
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm8/model/
H A Darm8AssemblerLib.sml75 fun ok r = (Portable.inc pc; mlibUseful.INR r) function
97 then ok w :: p1
102 | WORD w => ok w :: p1
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/
H A Dx64AssemblerLib.sml40 fun ok l = (incpc (List.length l); mlibUseful.INR l) function
58 | l => ok l :: p1)
64 | STREAM l => ok l :: p1
/seL4-l4v-10.1.1/HOL4/examples/elliptic/
H A DsubtypeTools.sml208 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-10.1.1/HOL4/tools/Holmake/
H A DHolmake_types.sml133 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 Dinternal_functions.sml58 val (ok, rest) = position (string from) ss value
61 recurse (to::ok::acc) (slice(rest, size from, NONE))
62 else concat (List.rev (ok::acc))
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/extract/
H A Dlisp_extractLib.sml386 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``)
391 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)``
450 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v args,fns,io,ok)``)
458 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) (ans,k2,io2,ok2)``
720 val lemma = DISCH_ALL (ASSUME ``R_ap (Fun ^name_tm,args,e,fns,io,ok) (^v (args,fns,io,ok))``)
721 |> DISCH ``^v2 (args,fns,io,ok)`` |> PURE_REWRITE_RULE [AND_IMP_INTRO]
727 val th2 = CS [R_ap_Fun] ``R_ap (Fun ^name_tm,^args,e,k,io,ok) re
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/Thy/
H A Dthy_resources.scala41 case Session.Terminated(result) if !result.ok =>
64 def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Thy/
H A Dthy_resources.scala41 case Session.Terminated(result) if !result.ok =>
64 def ok: Boolean = nodes.forall({ case (_, st) => st.ok })
/seL4-l4v-10.1.1/HOL4/src/1/
H A DThmSetData.sml151 val (ok,notok) = Lib.partition P alist value
161 data = #1 (mk (map #1 ok))})
/seL4-l4v-10.1.1/isabelle/src/Tools/VSCode/src/
H A Dserver.scala285 if (!build(no_build = true).ok) {
292 if (!build().ok) { progress.echo(fail_msg); error(fail_msg) }
323 case Session.Terminated(result) if !result.ok =>
354 if (result.ok) reply("") else reply("Prover shutdown failed: return code " + result.rc)

Completed in 206 milliseconds

123456