/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/regular-play/src/ |
H A D | regexSemanticsScript.sml | 65 (* ok, but not quite all - just 2 *)
|
/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/HOL4/src/parse/ |
H A D | GrammarDeltas.sml | 131 val (ok,notok) = Lib.partition check_delta deltas value 140 set_theory_data {thydataty = tmtag, data = toData ok})
|
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-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/bytecode/ |
H A D | lisp_compilerScript.sml | 32 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 D | dump.scala | 135 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 D | pretty_text_area.scala | 211 val (pattern, ok) = 223 if (ok) search_field_foreground
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/ |
H A D | dump.scala | 135 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 D | pretty_text_area.scala | 211 val (pattern, ok) = 223 if (ok) search_field_foreground
|
/seL4-l4v-10.1.1/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-10.1.1/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-10.1.1/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-10.1.1/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 | 58 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 D | lisp_extractLib.sml | 386 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 D | thy_resources.scala | 41 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 D | thy_resources.scala | 41 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 D | ThmSetData.sml | 151 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 D | server.scala | 285 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)
|