| /seL4-l4v-10.1.1/HOL4/examples/separationLogic/src/holfoot/ |
| H A D | selftest.sml | 29 val ok = snd ((holfootLib.holfoot_interactive_verify_spec (not quiet) (not quiet) (concat [examples_dir, file]) (SOME [generate_vcs]) [])); value
|
| /seL4-l4v-10.1.1/HOL4/src/portableML/monads/ |
| H A D | stmonad.sig | 7 val ok : ('a, unit) stmonad value
|
| H A D | stmonad.sml | 16 fun ok s = return () s function
|
| H A D | errormonad.sig | 10 val ok : ('a, unit, 'c) t value
|
| H A D | optmonad.sig | 8 val ok : ('a, unit) optmonad value
|
| H A D | seqmonad.sig | 8 val ok : ('a, unit) seqmonad value
|
| H A D | errormonad.sml | 12 fun ok e = return () e (* eta-expanded b/c of value restriction *) function
|
| H A D | optmonad.sml | 12 fun ok env = return () env function
|
| H A D | seqmonad.sml | 5 fun ok env = seq.result (env, ()) function
|
| /seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
| H A D | holdeptool.sml | 5 fun ok () = OS.Process.exit OS.Process.success function
|
| H A D | Holmake_types.sml | 133 val (ok, spaces) = splitr Char.isSpace ss value
|
| H A D | internal_functions.sml | 58 val (ok, rest) = position (string from) ss value
|
| /seL4-l4v-10.1.1/HOL4/src/parse/ |
| H A D | GrammarDeltas.sml | 131 val (ok,notok) = Lib.partition check_delta deltas value
|
| /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
|
| /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
|
| /seL4-l4v-10.1.1/HOL4/src/pattern_matches/ |
| H A D | selftest.sml | 35 val ok = if not (isSome out_opt) then not (isSome res_opt) else value
|
| /seL4-l4v-10.1.1/HOL4/src/quantHeuristics/ |
| H A D | selftest.sml | 25 val ok = if not (isSome r_opt) then not (isSome thm_opt) else value
|
| /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
|
| /seL4-l4v-10.1.1/HOL4/src/1/ |
| H A D | ThmSetData.sml | 151 val (ok,notok) = Lib.partition P alist value
|
| /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
|
| /seL4-l4v-10.1.1/HOL4/examples/muddy/muddyC/buddy/src/ |
| H A D | bddio.c | 384 int ok; local
478 int ok; local
|
| H A D | cppext.cxx | 83 int ok = bdd_init(n,c); local
424 int ok, first; local
|
| H A D | fdd.c | 739 int ok, first; local
|
| /seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/ |
| H A D | Solver.h | 53 bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! member in class:Solver
|
| /seL4-l4v-10.1.1/HOL4/src/simp/src/ |
| H A D | Cache.sml | 45 fun ok (prev,SOME thm) = prev << curr function
223 fun ok (cached, SOME _) = cached << hyps function
|