/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | ElementSet.sml | 310 fun adds acc set = foldl check acc set 312 and check (elt,acc) = function
|
H A D | Useful.sml | 605 fun check s = function 613 val () = check s 628 fun check s = function 636 val () = check s
|
/seL4-l4v-10.1.1/HOL4/src/parse/ |
H A D | selftest.sml | 356 fun check (s1,s2) = function 362 val f = PrecAnalysis.check_for_listreductions check 744 fun check (Exn.Res (SOME (r, _))) = function 746 | check _ = false 750 require_msg check pr (lex []) (qbuf.new_buffer [QUOTE s])
|
H A D | Parse_support.sml | 150 fun check i = i < 0 orelse (String.sub(s,i) = #"_" andalso check (i - 1)) function 152 check (size s - 1) 216 * Failing that, check to see if the string is a known constant.
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | OldPP.sml | 448 let fun check k = function 462 check(k-1)) 469 check(k + !Pend)) 475 then check k 478 in check 0
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | Regexp_Type.sml | 916 (* check that the list is non-empty. If it happens that the prefix is empty *) 1168 let fun check [] = true function 1169 | check ((g::_)::t) = h=g andalso check t 1170 | check other = false 1171 in check rst 1182 fun check [] = true function 1183 | check (L::t) = item=last L andalso check t 1184 in check rs [all...] |
/seL4-l4v-10.1.1/HOL4/src/postkernel/ |
H A D | Theory.sml | 552 axioms never have hypotheses (check type of new_axiom) *) 557 let fun check (_, Thm _ ) = true function 558 | check (_, Defn _) = true 559 | check (_, Axiom(_,th)) = uptodate_term (Thm.concl th) 561 update_seg s (U #facts (List.filter check facts)) $$ 565 let fun check (_, Axiom _) = true function 566 | check (_, Thm th ) = uptodate_thm th 567 | check (_, Defn th) = uptodate_thm th 569 update_seg s (U #facts (List.filter check facts)) $$
|
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/ |
H A D | basic.sml | 227 (* Sanity check of the source program. *)
|
/seL4-l4v-10.1.1/HOL4/examples/elliptic/ |
H A D | Useful.sml | 86 fun check () = function 98 check 609 fun check s = assert (String.isPrefix p s) (Error "dest_prefix") function 612 fn s => (check s; String.extract (s, size_p, NONE))
|
/seL4-l4v-10.1.1/HOL4/src/HolSmt/ |
H A D | Z3.sml | 115 (* parse the proof and check it in HOL *)
|
/seL4-l4v-10.1.1/HOL4/src/compute/Manual/ |
H A D | description.tex | 78 have been recognized, but it is mainly to check that everything was
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | OmegaShell.sml | 32 Before throwing ourselves into DNF-ication, we check to see if T
|
/seL4-l4v-10.1.1/HOL4/src/num/arith/src/ |
H A D | numSimps.sml | 447 fun check tm = let function 455 RCACHE (dp_vars, check, CTXT_ARITH) 456 (* the check function determines whether or not a term might be handled 544 Also check that theorem is not (SUC n = SUC m) = (n = m) *)
|
/seL4-l4v-10.1.1/HOL4/tools-poly/Holmake/ |
H A D | unix-systeml.sml | 114 (* Can't lift the check out of the function body because of the value
|
/seL4-l4v-10.1.1/HOL4/developers/ |
H A D | poly-prehol.sml | 189 ; PolyML.use (HOLDIR ++ "tools" ++ "check-intconfig.sml")
|
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/ |
H A D | ctlCheck.sml | 2 (* check ctl formulas via muCheck *)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/ |
H A D | isabelle_cronjob.scala | 58 Bash.string(backup + "/log") + " " + File.bash_path(main_dir)).check 69 .check
|
/seL4-l4v-10.1.1/isabelle/src/Pure/General/ |
H A D | ssh.scala | 420 execute("rm -r -f " + Bash.string(remote_dir)).check 423 execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Useful.sml | 605 fun check s = function 613 val () = check s 628 fun check s = function 636 val () = check s
|
/seL4-l4v-10.1.1/HOL4/polyml/basis/ |
H A D | ExnPrinter.sml | 73 (* Print a ref. Because refs can form circular structures we include a check for a loop here. *)
|
H A D | Word32In64.sml | 88 (* Use Word.scan but check that the result is in the range. *)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/ |
H A D | isabelle_cronjob.scala | 58 Bash.string(backup + "/log") + " " + File.bash_path(main_dir)).check 69 .check
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/ |
H A D | ssh.scala | 420 execute("rm -r -f " + Bash.string(remote_dir)).check 423 execute("mktemp -d -t tmp.XXXXXXXXXX").check.out
|
/seL4-l4v-10.1.1/seL4/manual/parts/ |
H A D | notifications.tex | 72 or an IPC, developers should check the badge value. By reserving a
|
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/m0/model/ |
H A D | m0AssemblerLib.sml | 126 fun check (add, label, line) x ast = function 138 val chk = check (!pc + 1 <= lpc, label, line)
|