Searched refs:check (Results 1 - 25 of 382) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/
H A DMakefile3 top: pkg-check.txt
11 pkg-check.txt: PKGS.lsp PKGS.sml
20 @echo "(note-chk-known-package-alist-success \"pkg-check.txt\" state)" >> $(TMPFILE)
22 @$(ACL2) < $(TMPFILE) > pkg-check.out 2> pkg-check.err
23 @if [ ! -e pkg-check.txt ]; then \
24 echo "FAILURE for pkg-check.txt" ; \
38 rm -f pkg-check.*
/seL4-l4v-10.1.1/isabelle/src/Pure/Tools/
H A Dcheck_keywords.scala14 check: Set[String],
21 position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
37 check: Set[String],
45 conflicts(keywords, check, arg._1, arg._2)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Tools/
H A Dcheck_keywords.scala14 check: Set[String],
21 position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
37 check: Set[String],
45 conflicts(keywords, check, arg._1, arg._2)
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DInt32.sml34 fun check i = function
43 val fromLarge = check o fromLarge
44 val fromInt = check o fromInt
46 val ~ = check o ~
47 val op * = check o op *
48 val op + = check o op +
49 val op - = check o op -
50 val op div = check o op div
51 val op mod = check o op mod
52 val quot = check
[all...]
/seL4-l4v-10.1.1/HOL4/src/parse/
H A Dbase_tokens.sml21 fun check p exnstring (s,loc) = let function
23 fun check ss = function
26 | SOME (c,ss) => if p c then check ss
29 check (full s)
32 val check_binary = check (fn c => c = #"0" orelse c = #"1")
34 val check_octal = check (fn c => #"0" <= c andalso c <= #"7")
36 val check_hex = check (fn c => (#"0" <= c andalso c <= #"9") orelse
42 val check_decimal = check Char.isDigit "Illegal numeral"
H A DPrecAnalysis.sml62 fun check_for_listreductions check rels =
72 check(l,s) = NONE
83 (case check(s, tk1) of
85 (case check(valOf left_opt, tk1) of
93 | SOME l => (case check(l,tk1) of
105 case check (valOf left_opt, tk1) of
107 (case check (s, tk1) of
122 (case check (l, tk1) of
135 case check (valOf left_opt, tk2) of
137 (case check(tk
[all...]
H A Dtestutils.sml130 fun timed f check x =
138 check res
186 fun check res = function
194 timed f check x
201 fun check (Res r) = false function
202 | check (Exn e) = checkexn e
204 require_msg check printresult testfn arg
/seL4-l4v-10.1.1/isabelle/src/Pure/General/
H A Dmercurial.scala41 hg.command("root").check
60 hg.command(cmd, args, repository = false).check
101 hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
104 hg.command("heads", opt_template(template), options).check.out_lines
107 hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
112 hg.command("manifest", opt_rev(rev), options).check.out_lines
115 hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
126 hg.command("pull", opt_rev(rev) + optional(remote), options).check
129 rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
132 opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", chec
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/General/
H A Dmercurial.scala41 hg.command("root").check
60 hg.command(cmd, args, repository = false).check
101 hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
104 hg.command("heads", opt_template(template), options).check.out_lines
107 hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
112 hg.command("manifest", opt_rev(rev), options).check.out_lines
115 hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
126 hg.command("pull", opt_rev(rev) + optional(remote), options).check
129 rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
132 opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", chec
[all...]
/seL4-l4v-10.1.1/HOL4/src/simp/src/
H A Dselftest.sml76 "Bounded rewrites branch, and bypass permutative loop check"
98 fun check (th1, th2) = function
103 "Bounded rewrites override mk_rewrites loop check"
104 check
115 fun check th = aconv (rhs (concl th)) ``f (x:'a):'a = z`` function
119 check
130 fun check th = not (aconv (rhs (concl th)) ``x:bool``) function
134 check
145 fun check th = aconv (rhs (concl th)) result function
147 infloop_protect "Congruence for conditional expressions" check doi
156 fun check th = aconv (rhs (concl th)) result function
167 fun check th = aconv (rhs (concl th)) result function
181 fun check (sgs, vfn) = let function
200 fun check th = th |> concl |> rhs |> aconv F function
210 fun check th = th |> concl |> rhs |> aconv F function
[all...]
/seL4-l4v-10.1.1/isabelle/src/Pure/Concurrent/
H A Dsynchronized.scala33 def check(x: A): Option[B] =
44 check(x) match {
51 check(state)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Concurrent/
H A Dsynchronized.scala33 def check(x: A): Option[B] =
44 check(x) match {
51 check(state)
/seL4-l4v-10.1.1/HOL4/src/1/theory_tests/
H A Dgithub115bScript.sml5 (* this theory is in the test-case solely to force Holmake to check that the
/seL4-l4v-10.1.1/isabelle/src/Pure/Admin/
H A Dremote_dmg.scala19 ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
23 " dmg.dmg").check
H A Dbuild_cygwin.scala40 File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check
59 " -czf " + Bash.string(archive) + " cygwin").check
H A Dbuild_polyml.scala131 """, redirect = true, echo = true).check
141 val lines = bash(root, ldd + " target/bin/poly").check.out_lines
153 bash(dir1, "./build " + platform, redirect = true, echo = true).check
180 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check
186 Bash.string("@executable_path/" + Path.explode(file).base_name) + " poly").check
H A Dbuild_release.scala93 echo = true).check
114 echo = true).check
156 Isabelle_System.bash(script, cwd = tmp_dir.file).check
158 Isabelle_System.gnutar(args, cwd = tmp_dir.file).check
171 " -s -c -a -d '~~/src/Benchmarks'", echo = true).check
H A Dother_isabelle.scala53 other_isabelle("components -a", redirect = true, echo = echo).check
56 Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/Admin/
H A Dremote_dmg.scala19 ssh.execute(cd + "mkdir root && tar -C root -xzf dmg.tar.gz").check
23 " dmg.dmg").check
H A Dbuild_cygwin.scala40 File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check
59 " -czf " + Bash.string(archive) + " cygwin").check
H A Dbuild_polyml.scala131 """, redirect = true, echo = true).check
141 val lines = bash(root, ldd + " target/bin/poly").check.out_lines
153 bash(dir1, "./build " + platform, redirect = true, echo = true).check
180 bash(target, "chrpath -r '$ORIGIN' poly", echo = true).check
186 Bash.string("@executable_path/" + Path.explode(file).base_name) + " poly").check
H A Dbuild_release.scala93 echo = true).check
114 echo = true).check
156 Isabelle_System.bash(script, cwd = tmp_dir.file).check
158 Isabelle_System.gnutar(args, cwd = tmp_dir.file).check
171 " -s -c -a -d '~~/src/Benchmarks'", echo = true).check
/seL4-l4v-10.1.1/HOL4/src/datatype/theory_tests/
H A Dndatatype_ind0Script.sml32 fun check (tac, t) = (tac([], t) before ignore (save_thm( function
37 val _ = map check [
/seL4-l4v-10.1.1/HOL4/src/HolSat/sat_solvers/minisat/
H A DMain.C205 bool check = false; local
226 check = true;
243 if (proof != NULL || check) S.proof = new Proof();
252 if (S.proof != NULL && check) printf("Checking proof...\n"), checkProof(S.proof);
284 if (compress) { // ...compress, and possibly check
288 if (check)
293 } else if (check) { // ...check
/seL4-l4v-10.1.1/HOL4/src/HolQbf/
H A DHolQbfLib.sml37 QbfCertificate.VALID _ => QbfCertificate.check t dict cert
52 QbfCertificate.check t dict cert
66 QbfCertificate.check t dict cert
83 val th = QbfCertificate.check t' dict cert

Completed in 164 milliseconds

1234567891011>>