/seL4-l4v-10.1.1/HOL4/polyml/modules/ |
H A D | Makefile.in | 118 RECURSIVE_TARGETS = all-recursive check-recursive cscopelist-recursive \ 524 check-am: all-am 525 check: check-recursive 627 .PHONY: $(am__recursive_targets) CTAGS GTAGS TAGS all all-am check \ 628 check-am clean clean-generic clean-libtool cscopelist-am ctags \
|
/seL4-l4v-10.1.1/HOL4/src/metis/ |
H A D | mlibTermorder.sml | 182 (* A partial order on equations, designed to be quick to check. *) 419 fun check eqns = function 426 (* Uncomment this check function to print out the linear arithmetic problems 433 val check = fn eqns => 435 val (t,r) = timed check eqns 451 if inconsistent (check (omega_eqns vars eqns)) then NONE
|
H A D | mlibSolver.sml | 218 fun schedule check slice read stat = 222 if not (check ()) then 261 fun check () = check_meter (!slice) function 269 fn goal => schedule check slce read stat (map (C init_subnode goal) cnodes)
|
/seL4-l4v-10.1.1/isabelle/src/Pure/System/ |
H A D | isabelle_system.scala | 53 if (_settings.isEmpty) init() // unsynchronized check 161 bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check 312 try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } 321 def hostname(): String = bash("hostname -s").check.out
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/System/ |
H A D | isabelle_system.scala | 53 if (_settings.isEmpty) init() // unsynchronized check 161 bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check 312 try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } 321 def hostname(): String = bash("hostname -s").check.out
|
/seL4-l4v-10.1.1/HOL4/src/res_quan/src/ |
H A D | res_quanLib.sml | 348 (* check st l : Fail with st if l is empty, otherwise return l. *) 351 local fun check st l = if null l then raise ERR "check" st else l function 386 val imps = check "RESQ_RES_THEN: no restricted quantification " ths 388 val res = check "RESQ_RES_THEN: no resolvents " l 389 val tacs = check "RESQ_RES_THEN: no tactics" (mapfilter ttac res) 478 (* check that tm is a <varstruct> where: 500 (* check that tm is a <lhs> where:
|
/seL4-l4v-10.1.1/HOL4/tools/Holmake/ |
H A D | parse_glob.sml | 109 fun check s = function 127 grab_word classnames >- check
|
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/translations/ |
H A D | translationsLib.sig | 46 * These functions translate some ltl problems to an check whether there is 61 * These functions translate some ltl problems to an check whether there is
|
/seL4-l4v-10.1.1/isabelle/src/Pure/PIDE/ |
H A D | resources.scala | 40 def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None 44 if (path.is_absolute || path.is_current) check(path) 46 check(Path.explode("~~/src/Pure") + path) orElse 48 else check(Path.explode("$ML_SOURCES") + path))
|
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/ |
H A D | Model.sig | 230 (* Note: if it's cheaper, a systematic check will be performed instead. *) 233 val check : value
|
H A D | Waiting.sml | 117 fun check ((parm,model),z) = function 121 val {T,F} = Model.check Model.interpretClause n model fv cl 126 List.foldl check 1.0 (zip parms models)
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Pure/PIDE/ |
H A D | resources.scala | 40 def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None 44 if (path.is_absolute || path.is_current) check(path) 46 check(Path.explode("~~/src/Pure") + path) orElse 48 else check(Path.explode("$ML_SOURCES") + path))
|
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Model.sig | 230 (* Note: if it's cheaper, a systematic check will be performed instead. *) 233 val check : value
|
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/regular/ |
H A D | regexp2dfa.sml | 327 fun check(J,lstring,name,string) = function 333 of ["-dfagen","SML",lstring,name,string] => check(regexpLib.SML,lstring,name,string) 334 | ["-dfagen","HOL",lstring,name,string] => check(regexpLib.HOL,lstring,name,string) 335 | [lstring,name,string] => check(justifyDefault, lstring, name,string)
|
/seL4-l4v-10.1.1/HOL4/src/HolQbf/ |
H A D | selftest.sml | 10 (* check whether Squolem is installed *)
|
/seL4-l4v-10.1.1/HOL4/src/tfl/src/ |
H A D | selftest.sml | 12 (* check parsability of quantified equation *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86/ |
H A D | x86_astScript.sml | 28 (* check whether rm requires a lock, i.e. specifies a memory access *)
|
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/x86_64/ |
H A D | x64_astScript.sml | 25 (* check whether rm requires a lock, i.e. specifies a memory access *)
|
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/ |
H A D | polystring.cpp | 154 int check = WideCharToMultiByte(codePage, 0, buffer, (int)buffLen, result->chars, outputLen, NULL, NULL); local 155 if (check <= 0) return EmptyString(mdTaskData);
|
/seL4-l4v-10.1.1/HOL4/src/integer/ |
H A D | intSimps.sml | 251 fun check tm = function 254 RCACHE (dpvars,check,CTXT_ARITH DP DPname) 255 (* the check function determines whether or not a term might be handled
|
/seL4-l4v-10.1.1/HOL4/src/portableML/ |
H A D | UTF8.sml | 114 check acc (pos + 1) pos (bc - 1) 117 and check acc pos start cnt = value 124 if isCont_char c then check acc (pos + 1) start (cnt - 1)
|
/seL4-l4v-10.1.1/HOL4/tools/ |
H A D | configure-mosml.sml | 107 fun check p = function 123 findpartial check paths 125 | NONE => if OS = "winNT" then check "." else NONE
|
/seL4-l4v-10.1.1/HOL4/tools-poly/ |
H A D | smart-configure.sml | 137 fun check p = function 153 findpartial check paths 155 | NONE => if OS = "winNT" then check "." else NONE
|
/seL4-l4v-10.1.1/graph-refine/ |
H A D | search.py | 11 import check namespace 12 from check import restr_others, loops_to_split, ProofNode 57 init_hyps = check.init_point_hyps (p) 87 def check (i): function in function:find_split_limit 106 map (check, check_order) 109 check (split) 742 hyps = check.init_point_hyps (p) 828 (r_start, r_step), 'Seq check failed')) 870 hyps = hyps + [check.non_r_err_pc_hyp (tags, 1187 hyp = check [all...] |
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64AssemblerLib.sml | 190 fun check false _ _ = NONE function 191 | check true l s = 204 | [(bs, s)] => (s, SOME (bs, check c l s))
|